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

    Abstract

    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)
    PublisherIEEE
    Publication date2012
    Pages98-105
    ISBN (Print)978-1-4673-4742-6
    DOIs
    Publication statusPublished - 2012
    Event2012 IEEE 14th International Symposium on High-Assurance Systems Engineering - Omaha, United States
    Duration: 25 Oct 201227 Oct 2012
    Conference number: 14
    https://ieeexplore.ieee.org/xpl/conhome/6374352/proceeding

    Conference

    Conference2012 IEEE 14th International Symposium on High-Assurance Systems Engineering
    Number14
    Country/TerritoryUnited States
    CityOmaha
    Period25/10/201227/10/2012
    Internet address
    SeriesI E E E International Symposium on High-Assurance Systems Engineering
    ISSN1530-2059

    Keywords

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

    Fingerprint

    Dive into the research topics of 'Using Stochastic Model Checking to Provision Complex Business Services'. Together they form a unique fingerprint.

    Cite this