基于CSP的UML活动图死锁和不确定性验证框架
A framework for verifying deadlock and nondeterminism in UML activity diagrams based on CSP
摘要：
在并发和分布式系统中，死锁和不确定性可能变得越来越难以检测。UML活动图是模拟顺序和并发行为的流程图。尽管UML社区广泛采用这种图，但是没有标准的方法来验证活动图中是否存在死锁和不确定性行为。非决定性在文献中通常被忽视，即使它可能被认为是一个非常相关的属性。本文提出了一个自动验证UML活动图中死锁和不确定性的框架。它为活动图引入了一种组合CSP语义，用于从UML模型自动生成CSP规范。这些规范是使用FDR细化检查器自动验证死锁和不确定性行为的输入。我们提出了一个插件的Astah建模环境，机械化的翻译过程中，并调用FDR在后台执行验证的属性。该工具保持了图与其CSP规范之间的可追溯性。它分析FDR结果以突出显示导致死锁或不确定行为的关系图路径。该框架为UML建模工具增加了验证功能，并保持形式化语义对用户透明。因此，用户在建模过程中不需要理解或操作形式符号。我们提出了一个案例研究的结果，适用于所提出的框架，在云计算领域的模型验证。我们讨论了未来的应用，由于我们的方法的潜力。
英文摘要：
Deadlock and nondeterminism may become increasingly hard to detect in concurrent and distributed systems. UML activity diagrams are flowcharts that model sequential and concurrent behavior. Although the UML community widely adopts such diagrams, there is no standard approach to verify the presence of deadlock and nondeterministic behavior in activity diagrams. Nondeterminism is usually neglected in the literature even though it may be considered a very relevant property. This work proposes a framework for the automatic verification of deadlock and nondeterminism in UML activity diagrams. It introduces a compositional CSP semantics for activity diagrams that is used to automatically generate CSP specifications from UML models. These specifications are the input for the automatic verification of deadlock and nondeterministic behavior using the FDR refinement checker. We propose a plugin for the Astah modeling environment that mechanizes the translation process, and that calls FDR in the background to perform the verification of properties. The tool keeps the traceability between a diagram and its CSP specification. It parses the FDR results to highlight the diagram paths that lead to a deadlock or a nondeterministic behavior. This framework adds verification capabilities to the UML modeling tool and keeps the formal semantics transparent to the users. Therefore, the user does not need to understand or manipulate formal notations during modeling. We present the results of a case study that applies the proposed framework for the verification of models in the domain of cloud computing. We discuss future applications due to the potential of our approach.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
