Analysing System Failure Behaviours with PRISM

X Ge; R F Paige; J A McDermid

doi:10.1109/SSIRI-C.2010.32

Analysing System Failure Behaviours with PRISM

X Ge, R F Paige, J A McDermid

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Other chapter contribution

Abstract

The verification of safety-critical systems using formal techniques is not something new. Traditionally, safety-critical systems are verified using hazard analysis techniques, e.g., fault tree analysis. As safety-critical systems have become larger and more complex, several analysis techniques with compositional capabilities were developed. However, these techniques were not able to analyse stochastic systems. In this paper, we present a model-based compositional safety analysis technique (i.e., failure propagation analysis) and explore the feasibility of integrating this safety analysis technique with techniques of probabilistic model checking, more precisely the PRISM model checker. By doing so, we make it possible to rigorously verify a model while system failure behaviours are quantitatively analysed.

Original language	English
Title of host publication	Proceedings of the 2010 Fourth International Conference on Secure Software Integration and Reliability Improvement Companion (SSIRI-C)
Pages	130-136
Number of pages	6
DOIs	https://doi.org/10.1109/SSIRI-C.2010.32
Publication status	Published - Jun 2010

Bibliographical note

2010 Fourth International Conference on Secure Software Integration and Reliability Improvement Companion (SSIRI-C)

Access to Document

10.1109/SSIRI-C.2010.32

Cite this

@inbook{9b67784bbf8143d6a010dd4beadc16af,

title = "Analysing System Failure Behaviours with PRISM",

abstract = "The verification of safety-critical systems using formal techniques is not something new. Traditionally, safety-critical systems are verified using hazard analysis techniques, e.g., fault tree analysis. As safety-critical systems have become larger and more complex, several analysis techniques with compositional capabilities were developed. However, these techniques were not able to analyse stochastic systems. In this paper, we present a model-based compositional safety analysis technique (i.e., failure propagation analysis) and explore the feasibility of integrating this safety analysis technique with techniques of probabilistic model checking, more precisely the PRISM model checker. By doing so, we make it possible to rigorously verify a model while system failure behaviours are quantitatively analysed.",

author = "X Ge and Paige, {R F} and McDermid, {J A}",

note = "2010 Fourth International Conference on Secure Software Integration and Reliability Improvement Companion (SSIRI-C)",

year = "2010",

month = jun,

doi = "10.1109/SSIRI-C.2010.32",

language = "English",

pages = "130--136",

booktitle = "Proceedings of the 2010 Fourth International Conference on Secure Software Integration and Reliability Improvement Companion (SSIRI-C)",

}

TY - CHAP

T1 - Analysing System Failure Behaviours with PRISM

AU - Ge, X

AU - Paige, R F

AU - McDermid, J A

N1 - 2010 Fourth International Conference on Secure Software Integration and Reliability Improvement Companion (SSIRI-C)

PY - 2010/6

Y1 - 2010/6

N2 - The verification of safety-critical systems using formal techniques is not something new. Traditionally, safety-critical systems are verified using hazard analysis techniques, e.g., fault tree analysis. As safety-critical systems have become larger and more complex, several analysis techniques with compositional capabilities were developed. However, these techniques were not able to analyse stochastic systems. In this paper, we present a model-based compositional safety analysis technique (i.e., failure propagation analysis) and explore the feasibility of integrating this safety analysis technique with techniques of probabilistic model checking, more precisely the PRISM model checker. By doing so, we make it possible to rigorously verify a model while system failure behaviours are quantitatively analysed.

AB - The verification of safety-critical systems using formal techniques is not something new. Traditionally, safety-critical systems are verified using hazard analysis techniques, e.g., fault tree analysis. As safety-critical systems have become larger and more complex, several analysis techniques with compositional capabilities were developed. However, these techniques were not able to analyse stochastic systems. In this paper, we present a model-based compositional safety analysis technique (i.e., failure propagation analysis) and explore the feasibility of integrating this safety analysis technique with techniques of probabilistic model checking, more precisely the PRISM model checker. By doing so, we make it possible to rigorously verify a model while system failure behaviours are quantitatively analysed.

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

U2 - 10.1109/SSIRI-C.2010.32

DO - 10.1109/SSIRI-C.2010.32

M3 - Other chapter contribution

SP - 130

EP - 136

BT - Proceedings of the 2010 Fourth International Conference on Secure Software Integration and Reliability Improvement Companion (SSIRI-C)

ER -

Analysing System Failure Behaviours with PRISM

Abstract

Bibliographical note

Access to Document

Other files and links

Cite this