基于CSP的UML活动图死锁与非确定性验证框架
软件工程
2019-10-31 v1
摘要
在并发与分布式系统中，死锁与非确定性可能变得愈发难以检测。UML活动图是刻画顺序与并发行为的流程图。尽管UML界广泛采用此类图，但尚无标准方法用于验证活动图中死锁与非确定性行为的存在。非确定性在文献中常被忽视，尽管它可被视为一种非常重要的性质。本文提出一种用于UML活动图死锁与非确定性自动验证的框架。它引入了活动图的组合式CSP语义，用于从UML模型自动生成CSP规约。这些规约作为使用FDR精化检验器自动验证死锁与非确定性行为的输入。我们提出了一种用于Astah建模环境的插件，将翻译过程机械化，并在后台调用FDR执行性质验证。该工具保持了图与其CSP规约之间的可追溯性。它解析FDR结果以高亮导致死锁或非确定性行为的图路径。该框架为UML建模工具增添了验证能力，并对用户保持形式化语义透明。因此，用户在建模过程中无需理解或操作形式化符号。我们展示了一个将所提框架应用于云计算领域模型验证的案例研究结果，并讨论了基于本方法潜力未来的应用。
引用
@article{arxiv.1910.13638,
title = {A framework for verifying deadlock and nondeterminism in UML activity diagrams based on CSP},
author = {Lucas Lima and Amaury Tavares and Sidney C. Nogueira},
journal= {arXiv preprint arXiv:1910.13638},
year = {2019}
}