Automatic failure analysis using safecharts

Yean Ru Chen, Pao Ann Hsiung

研究成果: Article同行評審

摘要

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 avoid such mishaps, we need to verify safety-critical systems thoroughly and formal verification techniques such as model checking are a very promising approach. However, modeling the systems formally is a challenging task, which is further aggravated by the necessity to model faults and automatic repairs in safety-critical systems. Currently, there is no automatic technique in formal verification that can aid system designers in formally modeling the faults and repairs. This work contributes by proposing an extension to the Safecharts model so that faults and repairs are easily modeled and then the Safecharts are transformed into semantically equivalent Extended Timed Automata models that can be directly model checked. In this way, automatic failure analysis techniques are integrated into the SGM model checker. Application examples show the feasibility and benefits of the proposed model-driven verification of safety-critical systems.

原文English
頁(從 - 到)57-78
頁數22
期刊International Journal of Software Engineering and Knowledge Engineering
17
發行號1
DOIs
出版狀態Published - 2007 2月

All Science Journal Classification (ASJC) codes

  • 軟體
  • 電腦網路與通信
  • 電腦繪圖與電腦輔助設計
  • 人工智慧

指紋

深入研究「Automatic failure analysis using safecharts」主題。共同形成了獨特的指紋。

引用此