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

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.