Verification and Implementation of Embedded Systems from High-Level Models

Abstract

Existing modelling tools for embedded systems analyze models that do not necessarily reflect executable code. We propose a holistic approach that includes visual modelling of the system and its environment, qualitative and quantitative verification of the model, and automated executable code generation. For high-level modelling, we introduce pCharts, a variant of hierarchical state machines with state invariants, probabilistic transitions, timed transitions, stochastic transitions, state costs, and transition costs. With embedded systems in mind, pCharts follow an event-centric interpretation, in which events are executable procedures, implying that their execution is fast enough that no queuing of events is needed. Our pCharts tool, pState, allows the whole system to be formally analyzed and code for executable parts generated. The goal is an automated approach from modelling and analysis to code generation. On a series of case studies, we demonstrate this technique. An off-the-shelf probabilistic model checker is used for analysis by compiling and transforming a hierarchical pCharts into a flat collection of probabilistic guarded commands with costs. From the pCharts model, also executable code that preserves the verified properties can be generated.