Workflow Fault Tree Generation Through Model Checking

Luke Thomas Herbert, Robin Sharp

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

862 Downloads (Pure)


We present a framework for the automated generation of fault trees from models of realworld process workflows, expressed in a formalised subset of the popular Business Process Modelling and Notation (BPMN) language. To capture uncertainty and unreliability in workflows, we extend this formalism with probabilistic non-deterministic branching. We present an algorithm that allows for exhaustive generation of possible error states that could arise in execution of the model, where the generated error states allow for both fail-stop behaviour and continued system execution. We employ stochastic model checking to calculate the probabilities of reaching each non-error system state. Each generated error state is assigned a variable indicating its individual probability of occurrence. Our method can determine the probability of combined faults occurring, while accounting for the basic probabilistic structure of the system being modelled. From these calculations, a comprehensive fault tree is generated. Further, we show that annotating the model with rewards (data) allows the expected mean values of reward structures to be calculated at points of failure.
Original languageEnglish
Title of host publicationSafety, Reliability and Risk Analysis: Beyond the Horizon : Proceedings
EditorsR.D.J.M. Steenbergen, P.H.A.J.M. van Gelder, S. Miraglia, A.C.W.M. Ton Vrouwenvelder
PublisherCRC Press
Publication date2014
ISBN (Print)978-1-138-00123-7
ISBN (Electronic)978-1-315-81559-6
Publication statusPublished - 2014
Event22nd ESREL conference - Amsterdam, Netherlands
Duration: 30 Sept 20132 Oct 2013
Conference number: 22


Conference22nd ESREL conference

Bibliographical note

22nd ESREL conference, Amsterdam, 30 September - 2 October 2013.


  • BPMN
  • Stochastic BPMN
  • Stochastic Model Checking
  • Quantitative Model Checking
  • Formal Risk Analysis
  • Fault Tree Analysis
  • Fault Tree Generation


Dive into the research topics of 'Workflow Fault Tree Generation Through Model Checking'. Together they form a unique fingerprint.

Cite this