Full Text:   <1551>

Summary:  <1128>

CLC number: TP311.5

On-line Access: 2018-01-11

Received: 2016-04-24

Revision Accepted: 2016-06-30

Crosschecked: 2017-11-29

Cited: 0

Clicked: 4009

Citations:  Bibtex RefMan EndNote GB/T7714

 ORCID:

Liang Dou

http://orcid.org/0000-0003-3044-3841

-   Go to

Article info.
Open peer comments

Frontiers of Information Technology & Electronic Engineering  2017 Vol.18 No.11 P.1773-1783

http://doi.org/10.1631/FITEE.1601196


Mechanized semantics and refinement of UML-Statecharts


Author(s):  Feng Sheng, Liang Dou, Zong-yuan Yang

Affiliation(s):  Department of Computer Science and Technology, East China Normal University, Shanghai 200241, China

Corresponding email(s):   fsheng1990@163.com, ldou@cs.ecnu.edu.cn, yzyuan@cs.ecnu.edu.cn

Key Words:  Unified Modeling Language (UML)-Statecharts, Coq, Refinement, Structured operational semantics


Feng Sheng, Liang Dou, Zong-yuan Yang. Mechanized semantics and refinement of UML-Statecharts[J]. Frontiers of Information Technology & Electronic Engineering, 2017, 18(11): 1773-1783.

@article{title="Mechanized semantics and refinement of UML-Statecharts",
author="Feng Sheng, Liang Dou, Zong-yuan Yang",
journal="Frontiers of Information Technology & Electronic Engineering",
volume="18",
number="11",
pages="1773-1783",
year="2017",
publisher="Zhejiang University Press & Springer",
doi="10.1631/FITEE.1601196"
}

%0 Journal Article
%T Mechanized semantics and refinement of UML-Statecharts
%A Feng Sheng
%A Liang Dou
%A Zong-yuan Yang
%J Frontiers of Information Technology & Electronic Engineering
%V 18
%N 11
%P 1773-1783
%@ 2095-9184
%D 2017
%I Zhejiang University Press & Springer
%DOI 10.1631/FITEE.1601196

TY - JOUR
T1 - Mechanized semantics and refinement of UML-Statecharts
A1 - Feng Sheng
A1 - Liang Dou
A1 - Zong-yuan Yang
J0 - Frontiers of Information Technology & Electronic Engineering
VL - 18
IS - 11
SP - 1773
EP - 1783
%@ 2095-9184
Y1 - 2017
PB - Zhejiang University Press & Springer
ER -
DOI - 10.1631/FITEE.1601196


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 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状态图的机械语义和精化研究

概要:UML(Unified Modeling Language)是业界建模与分析的事实标准。然而,由于UML的语义信息未被精确定义,我们无法对UML模型之间的精化关系进行验证。本文使用定理证明器Coq形式定义了UML状态图的语义和模型之间的精化关系,形成机械语义。基于机械语义,模型语义信息及精化关系可以被描述为谓词及定理,在定理证明器Coq中进行证明。此方法为可验证的、无错误的建模和精化提供了一个可行的方向。

关键词:UML状态图;Coq;精化;结构化操作语义

Darkslateblue:Affiliate; Royal Blue:Author; Turquoise:Article

Reference

[1]Andronick, J., Chetali, B., Ly, O., 2003. Using Coq to verify Java CardTM applet isolation properties. Proc. Int. Conf. on Theorem Proving in Higher Order Logics, p.335-351.

[2]Börger, E., Cavarra, A., Riccobene, E., 2000. Modeling the dynamics of UML state machines. Proc. Int. Workshop on Abstract State Machines, p.223-241.

[3]Broy, M., Cengarle, M., Rumpe, B., et al., 2007. Towards a System Model for UML: the Structural Data Model. http://rzbl04.biblio.etc.tu-bs.de:8080/docportal/servlets/MCRFileNodeServlet/DocPortal_derivate_00003898/Document_00018887.pdf

[4]Dou, L., Lu, L., Yang, Z., et al., 2013. Towards mechanized semantics of UML sequence diagrams and refinement relation. Proc. 24th IASTED Int. Conf. on Modelling and Simulation, p.262-269.

[5]Gonthier, G., 2007. The four colour theorem: engineering of a formal proof. Proc. 8th Asian Symp. on Computer Mathematics, p.333.

[6]Hallerstede, S., Snook, C., 2011. Refining nodes and edges of state machines. Proc. Int. Conf. on Formal Engineering Methods, p.569-584.

[7]Harel, D., Lachover, H., Naamad, A., et al., 1990. STATEMATE: a working environment for the development of complex reactive systems. IEEE Trans. Softw. Eng., 16(4):403-414.

[8]Jörjens, J., 2005. Secure Systems Development with UML. Springer-Verlag Berlin Heidelberg, Germany.

[9]Klein, C., Prehofer, C., Rumpe, B., 1997. Feature specification and refinement with state transition diagrams. Proc. 4th IEEE Workshop on Feature Interactions in Telecommunications Networks and Distributed Systems, p.284-297.

[10]Lano, K., Clark, D., 2008. Semantics and refinement of behavior state machines. Proc. 10th Int. Conf. on Enterprise Information Systems, p.42-49.

[11]Latella, D., Majzik, I., Massink, M., 1999. Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Form. Aspec. Comput., 11(6):637-664.

[12]Leroy, X., 2015. The CompCert C verified compiler: documentation and users manual. Inria, 16(5):563-576.

[13]Liu, S., Liu, Y., Andrö, E., et al., 2013. A formal semantics for complete UML state machines with communications. Proc. Int. Conf. on Integrated Formal Methods, p.331-346.

[14]Prehofer, C., 2013. Behavioral refinement and compatibility of statechart extensions. Electron. Notes Theor. Comput. Sci., 295:65-78.

[15]Said, M., Butler, M., Snook, C., 2009. Language and tool support for class and state machine refinement in UML-B. Proc. Int. Symp. on Formal Methods, p.579-595.

[16]Scholz, P., 2001. Incremental design of statechart specifications. Sci. Comput. Program., 40(1):119-145.

[17]Simons, A., 2000. On the compositional properties of UML statechart diagrams. Proc. Rigorous Object-Oriented Methods Conf., p.1-12.

[18]Snook, C., Butler, M., 2008. UML-B and Event-B: an integration of languages and tools. Proc. IASTED Int. Conf. on Software Engineering, p.336-341.

[19]Sun, M., Zhang, N., Barbosa, L., 2004. On semantics and refinement of UML statecharts: a coalgebraic view. Proc. 2nd Int. Conf. on Software Engineering and Formal Methods, p.164-173.

[20]von der Beeck, M., 2002. A structured operational semantics for UML-statecharts. Softw. Syst. Model., 1(2):130-141.

Open peer comments: Debate/Discuss/Question/Opinion

<1>

Please provide your name, email address and a comment





Journal of Zhejiang University-SCIENCE, 38 Zheda Road, Hangzhou 310027, China
Tel: +86-571-87952783; E-mail: cjzhang@zju.edu.cn
Copyright © 2000 - 2022 Journal of Zhejiang University-SCIENCE