Generation of safe optimised execution strategies for uml models

Luke Thomas Herbert, Zaza Nadja Lee Herbert-Hansen

    Research output: Contribution to conferencePaperResearchpeer-review


    When designing safety critical systems there is a need for verification of safety properties while ensuring system operations have a specific performance profile. We present a novel application of model checking to derive execution strategies, sequences of decisions at workflow branch points, for a fragment of the Unified Modelling Language (UML) statechart language which is extended to include modelling of workflows which exhibit stochastic behaviour. Strategy
    generation is made possible by performing model checking on specific permutations of the set of possible actions to generate adversaries which optimise a set of reward variables, while simultaneously observing constraints which encode any required safety properties and accounting for the underlying stochastic nature of the system. By evaluating quantitative properties of the generated adversaries we are able to construct an execution strategy which fully specifies, from any state in the system, the actions needed for an actor to achieve the optimal values of the quantitative goals. We show that our method is computationally feasible and apply it to an illustrative example featuring an industrial robot in the food industry. Our approach make it possible to readily test and debug a wide range of possible designs, thus creating a more effective development of a safety critical system.
    Original languageEnglish
    Publication date2016
    Number of pages9
    Publication statusPublished - 2016
    Event13 th International Conference on Probabilistic Safety Assessment and Management (PSAM 13) - Sheraton Grande Walkerhill, Seoul, Korea, Republic of
    Duration: 2 Oct 20167 Oct 2016


    Conference13 th International Conference on Probabilistic Safety Assessment and Management (PSAM 13)
    LocationSheraton Grande Walkerhill
    Country/TerritoryKorea, Republic of


    Dive into the research topics of 'Generation of safe optimised execution strategies for uml models'. Together they form a unique fingerprint.

    Cite this