论文部分内容阅读
随着UML在系统建模中的广泛使用，模型间的一致性问题越来越突出．目前解决此问题的形式化方法主要是将UML模型转换为现有检测工具的输入语言进行处理．其往往会引入冗余计算及处理语义差异的负载．针对顺序图和状态图的一致性问题，考虑到Büchi自动机在刻画反应式系统方面的优势，提出了基于Büchi自动机理论的验证方法。在对顺序图和状态图的处理上，特别是在顺序图的处理上，本文给出了相应的步骤和规则，使得Büchi自动机能够顺利地应用到一致性验证中．