对 UML 状态机进行形式化以实现自动验证 -- 综述
软件工程
2024-07-25 v1 计算机科学中的逻辑
摘要
统一建模语言（UML）是建模动态系统的标准。UML 行为状态机用于建模面向对象设计的动态行为。由对象管理组（OMG）维护的 UML 规范以自然语言（与形式语言相对）进行文档化。自然语言固有的模糊性可能导致所得状态机模型中存在不一致。形式化 UML 状态机规范旨在解决模糊性问题，并为软件设计师和开发者提供统一的视角。这种形式化也旨在为 UML 状态机模型的自动验证提供基础，这有助于在早期发现软件设计漏洞并降低开发成本。我们在此提供了一份综述，涵盖1997年至2021年间与为目的为在设计阶段对 UML 状态机语义进行形式化以进行模型检查相关的现有工作。
引用
@article{arxiv.2407.17215,
title = {Formalizing UML State Machines for Automated Verification -- A Survey},
author = {Étienne André and Shuang Liu and Yang Liu and Christine Choppy and Jun Sun and Jin Song Dong},
journal= {arXiv preprint arXiv:2407.17215},
year = {2024}
}
备注
This is the author version of the manuscript of the same name published in ACM Computing Surveys