UML Statecharts的模型检验方法

摘要：

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

关键词：UML(unified modeling language)、Statecharts、模型检验、ω自动机

所属期刊栏目：14

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金69973051,60233020,90104007;国家高技术研究发展计划863计划2001AA113202;教育部霍英东教育基金会高等院校青年教师基金71064

在线出版日期：2004-01-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：750-756