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.

翻译：概率模型检验是一种广泛使用的形式化验证技术，可自动验证概率模型的定性与定量性质。然而，对这类系统进行建模、编写对应性质并进行验证需要领域知识，这使得不具备相关知识的科研人员和工程师难以使用。已有研究扩展了UML活动图、开发了转换方法并实现了自动化配套工具，但这些研究不够全面且未完全开放，导致难以评估、扩展、适配和访问。本文提出了一种针对活动图的综合验证框架，包括：用于概率、时间和质量标注的新配置文件、活动图在三种马尔可夫模型中的语义解释，以及从活动图到PRISM语言的一组转换规则（由PRISM和Storm支持）。更为重要的是，我们开发了转换算法并基于模型技术将其实现于名为QASCAD的工具中，实现了全自动验证。我们评估了一个多机器人医院配送案例研究，并进一步评估了文献中的另外六个示例。综合来看，本工作通过提升评估性、可扩展性、适配性和可访问性，为活动图的验证做出了显著贡献。