基于机构的简单 UML 状态机在 CASL/SPASS 中的编码与验证
软件工程
2020-11-03 v1
摘要
本文首次给出了 UML 状态机在机构（institution）逻辑框架内的正确语义表示（此前的尝试均有缺陷）。将该表示新颖地编码为一阶逻辑，使得可通过众多定理证明器进行符号分析。UML 状态机是基于模型的系统工程的核心。迄今为止，状态机分析主要局限于模型检测，而状态机上的模型检测深受状态空间爆炸问题的困扰。本文所实现并展示的符号推理提供了一种强大的替代方案，能够处理大型甚至无限状态空间。文中给出了完整的证明。
引用
@article{arxiv.2011.00556,
title = {Institution-based Encoding and Verification of Simple UML State Machines in CASL/SPASS},
author = {Tobias Rosenberger and Saddek Bensalem and Alexander Knapp and Markus Roggenbach},
journal= {arXiv preprint arXiv:2011.00556},
year = {2020}
}