Generation of safe optimised execution strategies for uml models

Luke Thomas Herbert, Zaza Nadja Lee Herbert-Hansen

    Research output: Contribution to conferencePaperResearchpeer-review

    Abstract

    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

    Conference

    Conference13 th International Conference on Probabilistic Safety Assessment and Management (PSAM 13)
    LocationSheraton Grande Walkerhill
    CountryKorea, Republic of
    CitySeoul
    Period02/10/201607/10/2016

    Cite this

    Herbert, L. T., & Herbert-Hansen, Z. N. L. (2016). Generation of safe optimised execution strategies for uml models. Paper presented at 13 th International Conference on Probabilistic Safety Assessment and Management (PSAM 13), Seoul, Korea, Republic of.
    Herbert, Luke Thomas ; Herbert-Hansen, Zaza Nadja Lee. / Generation of safe optimised execution strategies for uml models. Paper presented at 13 th International Conference on Probabilistic Safety Assessment and Management (PSAM 13), Seoul, Korea, Republic of.9 p.
    @conference{4136613ae36247f19baf6f1ee450f011,
    title = "Generation of safe optimised execution strategies for uml models",
    abstract = "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. Strategygeneration 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.",
    author = "Herbert, {Luke Thomas} and Herbert-Hansen, {Zaza Nadja Lee}",
    year = "2016",
    language = "English",
    note = "13 th International Conference on Probabilistic Safety Assessment and Management (PSAM 13) ; Conference date: 02-10-2016 Through 07-10-2016",

    }

    Herbert, LT & Herbert-Hansen, ZNL 2016, 'Generation of safe optimised execution strategies for uml models' Paper presented at 13 th International Conference on Probabilistic Safety Assessment and Management (PSAM 13), Seoul, Korea, Republic of, 02/10/2016 - 07/10/2016, .

    Generation of safe optimised execution strategies for uml models. / Herbert, Luke Thomas; Herbert-Hansen, Zaza Nadja Lee.

    2016. Paper presented at 13 th International Conference on Probabilistic Safety Assessment and Management (PSAM 13), Seoul, Korea, Republic of.

    Research output: Contribution to conferencePaperResearchpeer-review

    TY - CONF

    T1 - Generation of safe optimised execution strategies for uml models

    AU - Herbert, Luke Thomas

    AU - Herbert-Hansen, Zaza Nadja Lee

    PY - 2016

    Y1 - 2016

    N2 - 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. Strategygeneration 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.

    AB - 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. Strategygeneration 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.

    M3 - Paper

    ER -

    Herbert LT, Herbert-Hansen ZNL. Generation of safe optimised execution strategies for uml models. 2016. Paper presented at 13 th International Conference on Probabilistic Safety Assessment and Management (PSAM 13), Seoul, Korea, Republic of.