Mechanized semantics and refinement of UML-Statecharts

Feng SHENG; Liang DOU; Zong-yuan YANG

doi:10.1631/FITEE.1601196

PDF(322 KB)

Front. Inform. Technol. Electron. Eng ›› 2017, Vol. 18 ›› Issue (11) : 1773-1783. DOI: 10.1631/FITEE.1601196

Article

Mechanized semantics and refinement of UML-Statecharts

Author information +

History +

Abstract

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 UMLStatecharts 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.

Keywords

Unified Modeling Language (UML)-Statecharts / Coq / Refinement / Structured operational semantics

Cite this article

EndNote

Ris (Procite)

Bibtex

Download citation ▾

Feng SHENG, Liang DOU, Zong-yuan YANG. Mechanized semantics and refinement of UML-Statecharts. Front. Inform. Technol. Electron. Eng, 2017, 18(11): 1773‒1783 https://doi.org/10.1631/FITEE.1601196