Rapid scenario-based simulation and model checking for embedded systems

Verification and validation (V&V) is critical and costly for high-assurance systems. Even though many formal specification techniques are available to verify various properties for embedded systems, it takes much effort to develop the state model and specify properties using temporal logic. This paper presents a process to rapidly generate the state model by simulating system scenarios, and formal model checking techniques can then be applied to the state model to verify various properties. Because system scenarios are widely used during embedded system development, the effort needed to develop the state model for the embedded system is thus greatly reduced. This paper presents how informal system scenarios can be formalized and used in simulation to generate the state model. The simulation tool developed is also capable of performing runtime checking such as completeness and consistency checking, and timing analysis. The state model generated can be mapped to UML's Statechart. Furthermore, this paper uses a pattern-based approach to specify properties to be checked rapidly. In this. way, various formal model checking techniques can be applied to the embedded system development. This paper uses an embedded system application to illustrate these concepts.