论文部分内容阅读
UML动态子图主要包括序列图和状态图等，它们在描述系统的行为方面应用广泛，但是半形式化的语义使它们不能直接进行形式化验证。Coq是目前主流的交互式定理证明器，用形式化的Coq规范来描述UML动态子图模型，可以在此基础上进行对模型的属性进行验证等工作。基于现有工作，提出将UML动态子图模型转换为Coq形式规范的框架，在元模型层次给出状态图和序列图的转换规则，介绍算法和原型工具实现。这种元模型层次的转换方法，保证了转换前后的语法正确性，为进一步分析验证提供了基础。