Modeling and automatic failure analysis of safety-critical systems using extended safecharts

Yean-Ru Chen, Pao Ann Hsiung, Sao Jie Chen

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

Abstract

With the rapid progress in science and technology, we find ubiquitous use of safety-critical systems in avionics, consumer electronics, and medical instruments. In such systems, unintentional design faults might result in injury or even death to human beings. To avoid such mishaps, we need to verify safetycritical systems thoroughly, where formal verification techniques such as model checking play a very promising role. Currently, there is practically no automatic technique in formal verification used to formally model system faults and repairs. This work contributes in proposing an extension to the Safecharts model, with which faults and repairs can be easily modeled. Moreover, these Safecharts can be directly transformed into semantically equivalent Extended Timed Automata models for model checking. That is, after these models were integrated into a model checker, such as our previously proposed State Graph Manipulators (SGM) model checker, we can verify safety-critical systems. An application example is run to show the feasibility and benefits of the proposed model-driven verification method for safety-critical systems. As observed, the checking results, such as witnesses of property specifications representing hazards, provide more concrete and useful failure analysis information than the conventional Fault Tree Analysis (FTA).

Original languageEnglish
Title of host publicationComputer Safety, Reliability, and Security - 26th International Conference, SAFECOMP 2007, Proceedings
Pages451-464
Number of pages14
Publication statusPublished - 2007 Dec 1
Event26th International Conference on Computer Safety, Reliability, and Security, SAFECOMP 2007 - Nuremberg, Germany
Duration: 2007 Sep 182007 Sep 21

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4680 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other26th International Conference on Computer Safety, Reliability, and Security, SAFECOMP 2007
CountryGermany
CityNuremberg
Period07-09-1807-09-21

Fingerprint

Safety-critical Systems
Failure Analysis
Failure analysis
Safety
Medical Electronics
Modeling
Fault
Formal Verification
Model checking
Model Checking
Repair
Model
Technology
Verify
Fault Tree Analysis
Fault tree analysis
Wounds and Injuries
Avionics
Consumer electronics
Timed Automata

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Chen, Y-R., Hsiung, P. A., & Chen, S. J. (2007). Modeling and automatic failure analysis of safety-critical systems using extended safecharts. In Computer Safety, Reliability, and Security - 26th International Conference, SAFECOMP 2007, Proceedings (pp. 451-464). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4680 LNCS).
Chen, Yean-Ru ; Hsiung, Pao Ann ; Chen, Sao Jie. / Modeling and automatic failure analysis of safety-critical systems using extended safecharts. Computer Safety, Reliability, and Security - 26th International Conference, SAFECOMP 2007, Proceedings. 2007. pp. 451-464 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{9f836202574a47109db17327c913a8d6,
title = "Modeling and automatic failure analysis of safety-critical systems using extended safecharts",
abstract = "With the rapid progress in science and technology, we find ubiquitous use of safety-critical systems in avionics, consumer electronics, and medical instruments. In such systems, unintentional design faults might result in injury or even death to human beings. To avoid such mishaps, we need to verify safetycritical systems thoroughly, where formal verification techniques such as model checking play a very promising role. Currently, there is practically no automatic technique in formal verification used to formally model system faults and repairs. This work contributes in proposing an extension to the Safecharts model, with which faults and repairs can be easily modeled. Moreover, these Safecharts can be directly transformed into semantically equivalent Extended Timed Automata models for model checking. That is, after these models were integrated into a model checker, such as our previously proposed State Graph Manipulators (SGM) model checker, we can verify safety-critical systems. An application example is run to show the feasibility and benefits of the proposed model-driven verification method for safety-critical systems. As observed, the checking results, such as witnesses of property specifications representing hazards, provide more concrete and useful failure analysis information than the conventional Fault Tree Analysis (FTA).",
author = "Yean-Ru Chen and Hsiung, {Pao Ann} and Chen, {Sao Jie}",
year = "2007",
month = "12",
day = "1",
language = "English",
isbn = "9783540751007",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "451--464",
booktitle = "Computer Safety, Reliability, and Security - 26th International Conference, SAFECOMP 2007, Proceedings",

}

Chen, Y-R, Hsiung, PA & Chen, SJ 2007, Modeling and automatic failure analysis of safety-critical systems using extended safecharts. in Computer Safety, Reliability, and Security - 26th International Conference, SAFECOMP 2007, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4680 LNCS, pp. 451-464, 26th International Conference on Computer Safety, Reliability, and Security, SAFECOMP 2007, Nuremberg, Germany, 07-09-18.

Modeling and automatic failure analysis of safety-critical systems using extended safecharts. / Chen, Yean-Ru; Hsiung, Pao Ann; Chen, Sao Jie.

Computer Safety, Reliability, and Security - 26th International Conference, SAFECOMP 2007, Proceedings. 2007. p. 451-464 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4680 LNCS).

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

TY - GEN

T1 - Modeling and automatic failure analysis of safety-critical systems using extended safecharts

AU - Chen, Yean-Ru

AU - Hsiung, Pao Ann

AU - Chen, Sao Jie

PY - 2007/12/1

Y1 - 2007/12/1

N2 - With the rapid progress in science and technology, we find ubiquitous use of safety-critical systems in avionics, consumer electronics, and medical instruments. In such systems, unintentional design faults might result in injury or even death to human beings. To avoid such mishaps, we need to verify safetycritical systems thoroughly, where formal verification techniques such as model checking play a very promising role. Currently, there is practically no automatic technique in formal verification used to formally model system faults and repairs. This work contributes in proposing an extension to the Safecharts model, with which faults and repairs can be easily modeled. Moreover, these Safecharts can be directly transformed into semantically equivalent Extended Timed Automata models for model checking. That is, after these models were integrated into a model checker, such as our previously proposed State Graph Manipulators (SGM) model checker, we can verify safety-critical systems. An application example is run to show the feasibility and benefits of the proposed model-driven verification method for safety-critical systems. As observed, the checking results, such as witnesses of property specifications representing hazards, provide more concrete and useful failure analysis information than the conventional Fault Tree Analysis (FTA).

AB - With the rapid progress in science and technology, we find ubiquitous use of safety-critical systems in avionics, consumer electronics, and medical instruments. In such systems, unintentional design faults might result in injury or even death to human beings. To avoid such mishaps, we need to verify safetycritical systems thoroughly, where formal verification techniques such as model checking play a very promising role. Currently, there is practically no automatic technique in formal verification used to formally model system faults and repairs. This work contributes in proposing an extension to the Safecharts model, with which faults and repairs can be easily modeled. Moreover, these Safecharts can be directly transformed into semantically equivalent Extended Timed Automata models for model checking. That is, after these models were integrated into a model checker, such as our previously proposed State Graph Manipulators (SGM) model checker, we can verify safety-critical systems. An application example is run to show the feasibility and benefits of the proposed model-driven verification method for safety-critical systems. As observed, the checking results, such as witnesses of property specifications representing hazards, provide more concrete and useful failure analysis information than the conventional Fault Tree Analysis (FTA).

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

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

M3 - Conference contribution

SN - 9783540751007

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 451

EP - 464

BT - Computer Safety, Reliability, and Security - 26th International Conference, SAFECOMP 2007, Proceedings

ER -

Chen Y-R, Hsiung PA, Chen SJ. Modeling and automatic failure analysis of safety-critical systems using extended safecharts. In Computer Safety, Reliability, and Security - 26th International Conference, SAFECOMP 2007, Proceedings. 2007. p. 451-464. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).