Mechanized semantics and refinement of UML-Statecharts  

作　　者：Feng SHENG Liang DOU Zong-yuan YANG 

机构地区：[1]Department of Computer Science and Technology, East China Normal University, Shanghai 200241, China

出　　处：《Frontiers of Information Technology & Electronic Engineering》2017年第11期1773-1783,共11页信息与电子工程前沿（英文版）

基　　金：Project supported by the National Natural Science Foundation of China （No. 61070226）

摘　　要：The Unified Modeling Language （UML） is an industry standard for modeling analysis and design. However, the semantics of UML is not precisely defined and the correctness of refinement relations cannot be verified. In this study, we use the theorem proof assistant Coq to formalize and mechanize the semantics of UML- Statecharts and the refinement relations between models. Based on the mechanized semantics, the desired properties of both the semantics and the refinement relations can be described and proven as predicates and lemmas. This approach provides a promising way to obtain certified fault-free modeling and refinement.UML(Unified Modeling Language)是业界建模与分析的事实标准。然而,由于UML的语义信息未被精确定义,我们无法对UML模型之间的精化关系进行验证。本文使用定理证明器Coq形式定义了UML状态图的语义和模型之间的精化关系,形成机械语义。基于机械语义,模型语义信息及精化关系可以被描述为谓词及定理,在定理证明器Coq中进行证明。此方法为可验证的、无错误的建模和精化提供了一个可行的方向。

关 键 词：Unified Modeling Language （UML）-Statecharts COQ REFINEMENT Structured operational semantics 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]