UMLStatecharts的模型检验方法

UMLStatecharts的模型检验方法 摘 要: 统一建模语言 UML 已广泛应用于软件开发中,验证 UML 模型是否满足某些关键性质成为一个重要 问题.提出了对 UML Statecharts 进行模型检验的方法.首先用扩展层次自动机结构化地表示 UML Statecharts,然 后给出其操作语义,通过寻找最大无冲突迁移集可以保证语义的正确性.对于具有无穷运行的系统,该操作语义 可以映射到一个 Büchi自动机.使用基于自动机理论的模型检验方法来验证 UML Statecharts 的线性时态逻辑性 质,并给出方法验证由 Statecharts 和协同图建模的复杂多对象系统.