元模型层次的UML动态子图到Coq形式规范的转换

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