Safecharts model checking for the verification of safety-critical systems

Pao Ann Hsiung, Yen Hung Lin, Yean Ru Chen

研究成果: Chapter

1 引文 斯高帕斯(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.

主出版物標題Verification, Validation and Testing in Software Engineering
發行者IGI Global
出版狀態Published - 2006

All Science Journal Classification (ASJC) codes

  • 電腦科學(全部)


深入研究「Safecharts model checking for the verification of safety-critical systems」主題。共同形成了獨特的指紋。