Home
Scholarly Works
Analysis and Implementation of Embedded System...
Chapter

Analysis and Implementation of Embedded System Models: Example of Tags in Item Management Application

Abstract

We use an application with electronic tags to illustrate a holistic development approach that includes visual modelling of the system and its environment, qualitative and quantitative verification of the model, and executable code generation. To this end, we use, pState, a tool for the design of hierarchical state machines extended with probabilistic transitions, costs/rewards, and state invariants, called pCharts. From a pChart model, pState generates input code for a probabilistic model checker in the form of either a Markov Decision Process or a Probabilistic Timed Automaton. On the generated model, qualitative and quantitative properties can be verified. From sub-charts without probabilistic transitions, pState can generate executable code in C or assembly language. We analyze the tag collection and collision arbitration of the DASH-7 open standard protocol in which message collision is allowed to some extent. First, we create a model of the tag collection to calculate the collision probability and then we use the collision probability to estimate the average tag power consumption. Finally, we show how the code for a tag micro-controller can be generated directly from an embedded system model.

Authors

Nokovic B; Sekerinski E

Book title

Model-Implementation Fidelity in Cyber Physical System Design

Pagination

pp. 175-199

Publisher

Springer Nature

Publication Date

January 1, 2016

DOI

10.1007/978-3-319-47307-9_7
View published work (Non-McMaster Users)

Contact the Experts team