计算机应用与软件2016，Vol.33Issue(8)：7-11,66,6.DOI:10.3969/j.issn.1000-386x.2016.08.002
元模型层次的 UML 动态子图到 Coq 形式规范的转换
A METAMODELLING LEVEL TRANSFORMATION FROM UML DYNAMIC SUB-DIAGRAMS TO COQ
摘要
Abstract
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 KermetaKey words
UML Dynamic diagrams/Model transformation/Metamodelling/Coq Kermeta分类
信息技术与安全科学引用本文复制引用
窦亮,尹敏,李超,杨宗源..元模型层次的 UML 动态子图到 Coq 形式规范的转换[J].计算机应用与软件,2016,33(8):7-11,66,6.基金项目
国家自然科学基金项目（61070226）。 （）
