Safecharts model checking for the verification of safety-critical systems

Pao Ann Hsiung, Yen Hung Lin, Yean Ru Chen

Research output: Chapter in Book/Report/Conference proceedingChapter

1 Citation (Scopus)


Unintentional design faults in safety-critical systems might result in injury or even death to human beings. However, the safety verification of such systems is getting very difficult because designs are becoming very complex. To cope with high design complexity, model-driven architecture (MDA) design is becoming a well-accepted trend. However, conventional methods of code testing and hazard analysis do not fit very well with MDA. To bridge this gap, we propose a safecharts model-based formal verification technique for safety-critical systems. The safety constraints in safecharts are mapped to semantic equivalents in timed automata. The theory for safety verification is proved and implemented in the SGM model checker. Prioritized and urgent transitions are implemented in SGM to model the safechart risk semantics. Finally, it is shown that priority-based approach to mutual exclusion of resource usage in safecharts is unsafe and solutions are proposed. Application examples show the benefits of the proposed model-driven verification method.

Original languageEnglish
Title of host publicationVerification, Validation and Testing in Software Engineering
PublisherIGI Global
Number of pages35
ISBN (Print)9781591408512
Publication statusPublished - 2006

All Science Journal Classification (ASJC) codes

  • General Computer Science


Dive into the research topics of 'Safecharts model checking for the verification of safety-critical systems'. Together they form a unique fingerprint.

Cite this