Analysing System Failure Behaviours with PRISM

Xiaocheng Ge, Richard F. Paige, John A. McDermid

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

12 Citations (Scopus)

Abstract

The verification of safety-critical systems using formal techniques is not something new[15]. 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 languageEnglish
Title of host publicationSSIRI-C 2010
Subtitle of host publicationThe Fourth IEEE International Conference on Secure Software Integration and Reliability Improvement Companion
Place of PublicationLos Alamitos
PublisherIEEE
Pages130-136
Number of pages7
ISBN (Electronic)9780769540870, 9781424476435
ISBN (Print)9781424476442
DOIs
Publication statusPublished - 26 Jul 2010
Externally publishedYes
Event4th IEEE International Conference on Secure Software Integration and Reliability Improvement Companion - Singapore, Singapore
Duration: 9 Jun 201011 Jun 2010
Conference number: 4
https://www.scimagojr.com/journalsearch.php?q=19700177339&tip=sid&clean=0

Conference

Conference4th IEEE International Conference on Secure Software Integration and Reliability Improvement Companion
Abbreviated titleSSIRI-C 2010
CountrySingapore
CitySingapore
Period9/06/1011/06/10
Internet address

Fingerprint Dive into the research topics of 'Analysing System Failure Behaviours with PRISM'. Together they form a unique fingerprint.

Cite this