Generation of safe optimised execution strategies for uml models

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.