使用Acceleo将UML状态机转换为有色Petri网：一份报告
软件工程
2014-05-07 v1 计算机科学中的逻辑
摘要
UML状态机被广泛用于指定动态系统行为。然而，其语义是非形式化描述的，因此阻碍了能够保证系统安全性的模型检测技术的应用。在先前的工作中，我们提出了一种使用有色Petri网对非并发UML状态机进行形式化的方法，以便进行形式化验证。在本文中，我们报告了使用模型到文本转换工具Acceleo以自动化方式实现此转换的经验。尽管Acceleo提供了有助于我们转换过程的特性，但它也存在难以克服的局限性。
引用
@article{arxiv.1405.1112,
title = {Translating UML State Machines to Coloured Petri Nets Using Acceleo: A Report},
author = {Étienne André and Mohamed Mahdi Benmoussa and Christine Choppy},
journal= {arXiv preprint arXiv:1405.1112},
year = {2014}
}
备注
In Proceedings ESSS 2014, arXiv:1405.0554