Towards the automated verification of weibull distributions for system failure rates

Yu Lu*, Alice A. Miller, Ruth Hoffmann, Christopher W. Johnson

*Corresponding author for this work

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

5 Citations (Scopus)

Abstract

Weibull distributions can be used to accurately model failure behaviours of a wide range of critical systems such as on-orbit satellite subsystems. Markov chains have been used extensively to model reliability and performance of engineering systems or applications. However, the exponentially distributed sojourn time of Continuous-Time Markov Chains (CTMCs) can sometimes be unrealistic for satellite systems that exhibit Weibull failures. In this paper, we develop novel semi-Markov models that characterise failure behaviours, based on Weibull failure modes inferred from realistic data sources. We approximate and encode these new models with CTMCs and use the PRISM probabilistic model checker. The key benefit of this integration is that CTMC-based model checking tools allow us to automatically and efficiently verify reliability properties relevant to industrial critical systems.

Original languageEnglish
Title of host publicationCritical Systems
Subtitle of host publicationFormal Methods and Automated Verification - Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2016, Proceedings
PublisherSpringer-Verlag
Pages81-96
Number of pages16
Volume9933 LNCS
ISBN (Print)9783319459424
DOIs
Publication statusPublished - 1 Jan 2016
Event21st International Workshop on Formal Methods for Industrial Critical Systems, FMICS-AVoCS 2016 and 16th International Workshop on Automated Verification of Critical Systems, AVoCS 2016 - Pisa, Italy
Duration: 26 Sept 201628 Sept 2016

Publication series

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

Conference

Conference21st International Workshop on Formal Methods for Industrial Critical Systems, FMICS-AVoCS 2016 and 16th International Workshop on Automated Verification of Critical Systems, AVoCS 2016
Country/TerritoryItaly
CityPisa
Period26/09/1628/09/16

Keywords

  • Continuous-time markov chains
  • Probabilistic model checking
  • Satellite systems
  • Semi-markov chains
  • Weibull distribution

Fingerprint

Dive into the research topics of 'Towards the automated verification of weibull distributions for system failure rates'. Together they form a unique fingerprint.

Cite this