论文标题
基于机构的编码和验证CASL/SPASS中简单的UML状态机器
Institution-based Encoding and Verification of Simple UML State Machines in CASL/SPASS
论文作者
论文摘要
本文在机构的逻辑框架内提供了UML状态计算机的第一个正确的语义表示（以前的尝试是有缺陷的）。将此表示形式编码为一阶逻辑的新颖编码可以通过众多定理 - 示波器进行符号分析。 UML状态机是基于模型的系统工程的核心。到目前为止，国家机器分析主要仅限于模型检查，该模型检查对国家空间爆炸问题的影响很大。如此处启用和演示，符号推理提供了一种强大的替代方案，可以处理大型甚至无限的状态空间。 给出了完整的证据。
This paper provides the first correct semantical representation of UML state-machines within the logical framework of an institution (previous attempts were flawed). A novel encoding of this representation into first-order logic enables symbolic analyses through a multitude of theorem-provers. UML state-machines are central to model-based systems-engineering. Till now, state-machine analysis has been mostly restricted to model checking, which for state-machines suffers heavily from the state-space explosion problem. Symbolic reasoning, as enabled and demonstrated here, provides a powerful alternative, which can deal with large or even infinite state spaces. Full proofs are given.
