摘要
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中进行证明。此方法为可验证的、无错误的建模和精化提供了一个可行的方向。
基金
Project supported by the National Natural Science Foundation of China （No. 61070226）
