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 Citations (Scopus)

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 IASTED International Conference on Software Engineering and Applications
EditorsM.H. Hamza
Pages568-573
Number of pages6
Volume7
StatePublished - 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

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

Model checking
Embedded systems
scenario
simulation
system development
Temporal logic
logic

Keywords

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

ASJC Scopus subject areas

  • Development
  • Software

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 IASTED International Conference on Software Engineering and Applications (Vol. 7, pp. 568-573)

Rapid scenario-based simulation and model checking for embedded systems. / Tsai, W. T.; Yu, Lian; Paul, Ray; Fan, Chun; Liu, Xinxin; Cao, Zhibin.

Proceedings of the IASTED International Conference on Software Engineering and Applications. ed. / M.H. Hamza. Vol. 7 2003. p. 568-573.

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

Tsai, WT, Yu, L, Paul, R, Fan, C, Liu, X & Cao, Z 2003, Rapid scenario-based simulation and model checking for embedded systems. in MH Hamza (ed.), Proceedings of the IASTED International Conference on Software Engineering and Applications. vol. 7, pp. 568-573, Proceedings of the Seventh IASTED International Conference on Software Engineering and Applications, Marina del Rey, CA, United States, 11/3/03.
Tsai WT, Yu L, Paul R, Fan C, Liu X, Cao Z. Rapid scenario-based simulation and model checking for embedded systems. In Hamza MH, editor, Proceedings of the IASTED International Conference on Software Engineering and Applications. Vol. 7. 2003. p. 568-573
Tsai, W. T. ; Yu, Lian ; Paul, Ray ; Fan, Chun ; Liu, Xinxin ; Cao, Zhibin. / Rapid scenario-based simulation and model checking for embedded systems. Proceedings of the IASTED International Conference on Software Engineering and Applications. editor / M.H. Hamza. Vol. 7 2003. pp. 568-573
@inproceedings{c5900d04050c47a488bb108da1de47f9,
title = "Rapid scenario-based simulation and model checking for embedded systems",
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.",
keywords = "Model checking, Simulation, State machines, System scenarios, Temporal logic, Verification and validation",
author = "Tsai, {W. T.} and Lian Yu and Ray Paul and Chun Fan and Xinxin Liu and Zhibin Cao",
year = "2003",
language = "English (US)",
isbn = "0889863946",
volume = "7",
pages = "568--573",
editor = "M.H. Hamza",
booktitle = "Proceedings of the IASTED International Conference on Software Engineering and Applications",

}

TY - GEN

T1 - Rapid scenario-based simulation and model checking for embedded systems

AU - Tsai, W. T.

AU - Yu, Lian

AU - Paul, Ray

AU - Fan, Chun

AU - Liu, Xinxin

AU - Cao, Zhibin

PY - 2003

Y1 - 2003

N2 - 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.

AB - 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.

KW - Model checking

KW - Simulation

KW - State machines

KW - System scenarios

KW - Temporal logic

KW - Verification and validation

UR - http://www.scopus.com/inward/record.url?scp=1542433695&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=1542433695&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:1542433695

SN - 0889863946

SN - 9780889863941

VL - 7

SP - 568

EP - 573

BT - Proceedings of the IASTED International Conference on Software Engineering and Applications

A2 - Hamza, M.H.

ER -