Model checking safety-critical systems using safecharts

Pao Ann Hsiung, Yean Ru Chen, Yen Hung Lin

研究成果: Article同行評審

26 引文 斯高帕斯(Scopus)

摘要

With rapid developments in science and technology, we now see the ubiquitous use of different types of safety-critical systems in our daily lives such as in avionics, consumer electronics, and medical systems. In such systems, unintentional design faults might result in injury or even death to human beings. To make sure that safety-critical systems are really safe, there is a need to verify them formally. However, the verification of such systems is getting more and more difficult because designs are becoming very complex. To cope with high design complexity, currently, model-driven architecture design is becoming a well-accepted trend. However, existing methods of testing and standards conformance are restricted to implementation code, so they do not fit very well with model-based approaches. To bridge this gap, we propose a model-based formal verification technique for safety-critical systems. In this work, the model-checking paradigm is applied to the Safecharts model, which was used for modeling but not yet used for verification. Our contributions listed are as follows: First, the safety constraints in Safecharts are mapped to semantic equivalents in timed automata for verification. Second, the theory for safety constraint verification is proven and implemented in a compositional model checker (that is, the State-Graph Manipulator (SGM)). Third, prioritized and urgent transitions are implemented in SGM to model the risk semantics in Safecharts. Finally, it is shown that the priority-based approach to mutual exclusion of resource usage in the original Safecharts is unsafe and corresponding solutions are proposed here. Application examples show the feasibility and benefits of the proposed model-driven verification of safety-critical systems.

原文English
頁(從 - 到)692-705
頁數14
期刊IEEE Transactions on Computers
56
發行號5
DOIs
出版狀態Published - 2007 5月

All Science Journal Classification (ASJC) codes

  • 軟體
  • 理論電腦科學
  • 硬體和架構
  • 計算機理論與數學

指紋

深入研究「Model checking safety-critical systems using safecharts」主題。共同形成了獨特的指紋。

引用此