Rapid scenario-based simulation and model checking for embedded systems

W. T. Tsai, Lian Yu, Ray Paul, Chun Fan, Xinxin Liu, Zhibin Cao

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationProceedings of the Seventh IASTED International Conference on Software Engineering and Applications
EditorsM.H. Hamza
Pages568-573
Number of pages6
StatePublished - Dec 1 2003
EventProceedings of the Seventh IASTED International Conference on Software Engineering and Applications - Marina del Rey, CA, United States
Duration: Nov 3 2003Nov 5 2003

Publication series

NameProceedings of the IASTED International Conference on Software Engineering and Applications
Volume7

Other

OtherProceedings of the Seventh IASTED International Conference on Software Engineering and Applications
CountryUnited States
CityMarina del Rey, CA
Period11/3/0311/5/03

    Fingerprint

Keywords

  • Model checking
  • Simulation
  • State machines
  • System scenarios
  • Temporal logic
  • Verification and validation

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Tsai, W. T., Yu, L., Paul, R., Fan, C., Liu, X., & Cao, Z. (2003). Rapid scenario-based simulation and model checking for embedded systems. In M. H. Hamza (Ed.), Proceedings of the Seventh IASTED International Conference on Software Engineering and Applications (pp. 568-573). (Proceedings of the IASTED International Conference on Software Engineering and Applications; Vol. 7).