Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Quantitative Assurance and Synthesis of Controllers from Activity Diagrams

Kangfeng Ye, Fang Yan, Simos Gerasimou

TL;DR

A comprehensive verification framework for ADs is proposed, including a new profile for probability, time, and quality annotations, a semantics interpretation of ADs in three Markov models, and a set of transformation rules from activity diagrams to the PRISM language, supported by PRISM and Storm.

Abstract

Probabilistic model checking is a widely used formal verification technique to automatically verify qualitative and quantitative properties for probabilistic models. However, capturing such systems, writing corresponding properties, and verifying them require domain knowledge. This makes it not accessible for researchers and engineers who may not have the required knowledge. Previous studies have extended UML activity diagrams (ADs), developed transformations, and implemented accompanying tools for automation. The research, however, is incomprehensive and not fully open, which makes it hard to be evaluated, extended, adapted, and accessed. In this paper, we propose a comprehensive verification framework for ADs, including a new profile for probability, time, and quality annotations, a semantics interpretation of ADs in three Markov models, and a set of transformation rules from activity diagrams to the PRISM language, supported by PRISM and Storm. Most importantly, we developed algorithms for transformation and implemented them in a tool, called QASCAD, using model-based techniques, for fully automated verification. We evaluated one case study where multiple robots are used for delivery in a hospital and further evaluated six other examples from the literature. With all these together, this work makes noteworthy contributions to the verification of ADs by improving evaluation, extensibility, adaptability, and accessibility.

Quantitative Assurance and Synthesis of Controllers from Activity Diagrams

TL;DR

A comprehensive verification framework for ADs is proposed, including a new profile for probability, time, and quality annotations, a semantics interpretation of ADs in three Markov models, and a set of transformation rules from activity diagrams to the PRISM language, supported by PRISM and Storm.

Abstract

Probabilistic model checking is a widely used formal verification technique to automatically verify qualitative and quantitative properties for probabilistic models. However, capturing such systems, writing corresponding properties, and verifying them require domain knowledge. This makes it not accessible for researchers and engineers who may not have the required knowledge. Previous studies have extended UML activity diagrams (ADs), developed transformations, and implemented accompanying tools for automation. The research, however, is incomprehensive and not fully open, which makes it hard to be evaluated, extended, adapted, and accessed. In this paper, we propose a comprehensive verification framework for ADs, including a new profile for probability, time, and quality annotations, a semantics interpretation of ADs in three Markov models, and a set of transformation rules from activity diagrams to the PRISM language, supported by PRISM and Storm. Most importantly, we developed algorithms for transformation and implemented them in a tool, called QASCAD, using model-based techniques, for fully automated verification. We evaluated one case study where multiple robots are used for delivery in a hospital and further evaluated six other examples from the literature. With all these together, this work makes noteworthy contributions to the verification of ADs by improving evaluation, extensibility, adaptability, and accessibility.
Paper Structure (54 sections, 5 equations, 29 figures, 5 tables, 4 algorithms)

This paper contains 54 sections, 5 equations, 29 figures, 5 tables, 4 algorithms.

Table of Contents

  1. Introduction
  2. Background
  3. UML Activity Diagrams
  4. Markov Chains and Markov Decision Processes
  5. PRISM Language and Probabilistic Model Checkers
  6. Motivating Hospital Intralogistics Scenario
  7. Properties
  8. Overview of our approach
  9. New profile and stereotypes
  10. Semantics of activity diagrams
  11. Semantics of activity diagrams
  12. Assumptions and well-formedness conditions
  13. General interpretation
  14. Assumptions.
  15. Semantics in Markov models
  16. ...and 39 more sections

Figures (29)

  • Figure 1: Activity diagram metamodel.
  • Figure 2: A subset of SysML activity notations.
  • Figure 3: The PRISM model of a two-dimensional random walk: four constant variables, one global variable, two modules (one local variable and four commands for each module), and one transition reward.
  • Figure 4: Model construction and build in PRISM
  • Figure 5: The corresponding system module to the two-dimensional random walk in Fig. \ref{['fig:prism_model_trw']}.
  • ...and 24 more figures

Theorems & Definitions (6)

  • definition 2 . 1: Markov chain and Markov property
  • definition 2 . 2: Discrete-Time Markov chains
  • definition 2 . 3: Cost and rewards
  • definition 2 . 4: Continuous-Time Markov chains
  • definition 2 . 5: Markov decision processes
  • remark 3 . 1