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

摘要

UML dynamic sub-diagrams mainly comprise the sequence diagram and the state machine diagram,they are widely applied in describing system behaviours.However,it is hard to perform direct formal verification due to the semi-formal semantics of UML.Coq is a mainstream interactive theorem prover,using formal Coq specification to describe UML dynamic sub-diagrams model can carry out verification on model’s attributes on that basis.According to our previous work,the paper presents a framework to transform UML dynamic sub-diagrams model to Coq formal specifications,and the transformation rules of UML sequence diagram and state machine diagram are offered at meta-modelling level.The algorithm and the implementation of prototype tool are also introduced.This metamodelling level transformation framework ensures the correctness of semantics before and after transformation,and lays the basis for further analysis and verification.%UML 动态子图主要包括序列图和状态图等，它们在描述系统的行为方面应用广泛，但是半形式化的语义使它们不能直接进行形式化验证。Coq 是目前主流的交互式定理证明器，用形式化的 Coq 规范来描述 UML 动态子图模型，可以在此基础上进行对模型的属性进行验证等工作。基于现有工作，提出将 UML 动态子图模型转换为 Coq 形式规范的框架，在元模型层次给出状态图和序列图的转换规则，介绍算法和原型工具实现。这种元模型层次的转换方法，保证了转换前后的语法正确性，为进一步分析验证提供了基础。