计算机应用与软件2017，Vol.34Issue(2)：1-7,47,8.DOI:10.3969/j.issn.1000-386x.2017.02.001
UML类图的形式规约与精化研究
FORMAL SPECIFICATION AND REFINEMENT FOR UML CLASS DIAGRAM
摘要
Abstract
The Unified Modeling Language (UML) is an important part of Modeling-driven engineering (MDE) because of its variety of well-known and intuitive graphical notations.However,the semantics of UML is not precisely defined and the correctness of refinements cannot be verified,which makes it difficult to verify in formal of the UML model.As the static model of describing system structure,UML class diagram has no complete formal semantics.Thus,using the theorem proof assistant Coq to formalize and mechanize the semantics of the UML class diagram and the refinements between the models.The syntactic structure and the semantics of the UML class diagram can be transformed to the rigorous definitions in Coq,which is called mechanized semantics.Besides,the structural refinement operations of the class diagram are also provided.The refinement relations between models can be formally defined in Coq,and the desired properties of the refinement relations can be proven to verify the correctness of the refinements,ensuring the consistency of structure and semantics before and after refining.Combining the UML and formal method,the theoretical foundation in the software developing process is provided.关键词
UML类图/模型精化/Coq机械语意Key words
UML class diagram/Model refinement/Coq Mechanized semantics分类
信息技术与安全科学引用本文复制引用
王博文,盛枫,窦亮,杨宗源..UML类图的形式规约与精化研究[J].计算机应用与软件,2017,34(2):1-7,47,8.基金项目
国家自然科学基金项目(61070226). （61070226）
