Using Stochastic Model Checking to Provision Complex Business Services

Luke Thomas Herbert, Robin Sharp

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


    We present a framework for modelling and analysis of real-world business workflows. Business processes regularly form the basis for the design of software services, and frequently display complex stochastic behaviour. The accurate evaluation of their qualitative aspects can allow for determining bounds on resources consumed during execution of business processes. Accurate resource provisioning is often central to ensuring the safe execution of a process. We first introduce a formalised core subset of the Business Process Modelling and Notation (BPMN), which we extend with probabilistic and non-deterministic branching and reward annotations. We then develop an algorithm for the efficient translation of these models into the guarded command language used by the model checker PRISM, in turn enabling model checking of BPMN processes and allowing for the calculation of a wide range of quantitative properties of business processes including transient probabilities, timing, occurrence and ordering of events, and best- and worst-case scenarios. The developments presented are illustrated using an example from the health-care industry.
    Original languageEnglish
    Title of host publication2012 IEEE 14th International Symposium on High-Assurance Systems Engineering (HASE)
    Publication date2012
    ISBN (Print)978-1-4673-4742-6
    Publication statusPublished - 2012
    Event14th IEEE International Symposium on High-Assurance Systems Engineering (HASE 2012) - Omaha, Nebraska, United States
    Duration: 25 Oct 201227 Oct 2012


    Conference14th IEEE International Symposium on High-Assurance Systems Engineering (HASE 2012)
    CountryUnited States
    CityOmaha, Nebraska
    SeriesI E E E International Symposium on High-Assurance Systems Engineering


    • BPMN
    • Probabilistic BPMN
    • Stochastic Model Checking
    • Service Engineering
    • Quantitative Service Analysis
    • Service Provisioning

    Cite this