Mechanized semantics and refinement of UML-Statecharts

Feng SHENG; Liang DOU; Zong-yuan YANG

doi:10.1631/FITEE.1601196

Your Location：

Home >

Browse articles >

Mechanized semantics and refinement of UML-Statecharts

Regular Papers | Updated：2022-05-19

- Mechanized semantics and refinement of UML-Statecharts
- UML状态图的机械语义和精化研究
- Frontiers of Information Technology & Electronic Engineering Vol. 18, Issue 11, Pages: 1773-1783(2017)
- Affiliations：
  
  Department of Computer Science and Technology, East China Normal University, Shanghai 200241, China
- Author bio：
  
  [ "Feng SHENG, E-mail: fsheng1990@163.com" ]
  Liang DOU, E-mail: ldou@cs.ecnu.edu.cn
  [ "Zong-yuan YANG, E-mail: yzyuan@cs.ecnu.edu.cn" ]
- Funds：
- DOI：10.1631/FITEE.1601196
  CLC： TP311.5
- Received：24 April 2016，
  
  Revised：2017-11-29，
  
  Published：2017-11
- Accepted：
Scan QR Code
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.
DOI：

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. DOI： 10.1631/FITEE.1601196.

摘要

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

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.

关键词

Keywords

references

J. Andronick , , , B. Chetali , , , O. Ly . . Using Coq to verify Java CardTM applet isolation properties . . Proc. Int. Conf. on Theorem Proving in Higher Order Logics , , 2003 . . p.335 - - 351 . . DOI: 10.1007/10930755_22 http://doi.org/10.1007/10930755_22 . .

E. Börger , , , A. Cavarra , , , E. Riccobene . . Modeling the dynamics of UML state machines . . Proc. Int. Workshop on Abstract State Machines , , 2000 . . p.223 - - 241 . . DOI: 10.1007/3-540-44518-8_13 http://doi.org/10.1007/3-540-44518-8_13 . .

M. Broy , , , M. Cengarle , , , B. Rumpe , , , 等 . . 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 http://rzbl04.biblio.etc.tu-bs.de:8080/docportal/servlets/MCRFileNodeServlet/DocPortal_derivate_00003898/Document_00018887.pdf , , 2007 . . .

L. Dou , , , L. Lu , , , Z. Yang , , , 等 . . Towards mechanized semantics of UML sequence diagrams and refinement relation . . Proc. 24th IASTED Int. Conf. on Modelling and Simulation , , 2013 . . p.262 - - 269 . . DOI: 10.2316/P.2013.802-021 http://doi.org/10.2316/P.2013.802-021 . .

G. Gonthier . . The four colour theorem: engineering of a formal proof . . Proc. 8th Asian Symp. on Computer Mathematics , , 2007 . . p.333 DOI: 10.1007/978-3-540-87827-8_28 http://doi.org/10.1007/978-3-540-87827-8_28 . .

S. Hallerstede , , , C. Snook . . Refining nodes and edges of state machines . . Proc. Int. Conf. on Formal Engineering Methods , , 2011 . . p.569 - - 584 . . DOI: 10.1007/978-3-642-24559-6_38 http://doi.org/10.1007/978-3-642-24559-6_38 . .

D. Harel , , , H. Lachover , , , A. Naamad , , , 等 . . STATEMATE: a working environment for the development of complex reactive systems . . IEEE Trans. Softw. Eng. , , 1990 . . 16 ( ( 4 ): ): 403 - - 414 . . DOI: 10.1109/32.54292 http://doi.org/10.1109/32.54292 . .

J. Jürjens . . Secure Systems Development with UML . . Springer-Verlag Berlin Heidelberg, Germany , , 2005 . . DOI: 10.1007/b137706 http://doi.org/10.1007/b137706 . .

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

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

D. Latella , , , I. Majzik , , , M. Massink . . Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker . . Form. Aspec. Comput. , , 1999 . . 11 ( ( 6 ): ): 637 - - 664 . . DOI: 10.1007/s001659970003 http://doi.org/10.1007/s001659970003 . .

X. Leroy . . The CompCert C verified compiler: documentation and user's manual . . Inria , , 2015 . . 16 ( ( 5 ): ): 563 - - 576 . . . .

S. Liu , , , Y. Liu , , , E. André , , , 等 . . A formal semantics for complete UML state machines with communications . . Proc. Int. Conf. on Integrated Formal Methods , , 2013 . . p.331 - - 346 . . DOI: 10.1007/978-3-642-38613-8_23 http://doi.org/10.1007/978-3-642-38613-8_23 . .

C. Prehofer . . Behavioral refinement and compatibility of statechart extensions . . Electron. Notes Theor. Comput. Sci. , , 2013 . . 295 65 - - 78 . . DOI: 10.1016/j.entcs.2013.04.006 http://doi.org/10.1016/j.entcs.2013.04.006 . .

M. Said , , , M. Butler , , , C. Snook . . Language and tool support for class and state machine refinement in UMLB . . Proc. Int. Symp. on Formal Methods , , 2009 . . p.579 - - 595 . . DOI: 10.1007/978-3-642-05089-3_37 http://doi.org/10.1007/978-3-642-05089-3_37 . .

P. Scholz . . Incremental design of statechart specifications . . Sci. Comput. Program. , , 2001 . . 40 ( ( 1 ): ): 119 - - 145 . . DOI: 10.1016/S0167-6423(00)00026-5 http://doi.org/10.1016/S0167-6423(00)00026-5 . .

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

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

M. Sun , , , N. Zhang , , , L. Barbosa . . On semantics and refinement of UML statecharts: a coalgebraic view . . Proc. 2nd Int. Conf. on Software Engineering and Formal Methods , , 2004 . . p.164 - - 173 . . DOI: 10.1109/SEFM.2004.1347517 http://doi.org/10.1109/SEFM.2004.1347517 . .

M. von der Beeck . . A structured operational semantics for UML-statecharts . . Softw. Syst. Model. , , 2002 . . 1 ( ( 2 ): ): 130 - - 141 . . DOI: 10.1007/s10270-002-0012-8 http://doi.org/10.1007/s10270-002-0012-8 . .

Views

Downloads

CSCD

Alert me when the article has been cited

Submit

Tools

Publicity Resources

No data

Related Author

No data

Related Institution

No data

Chat

Address：Zhejiang University Press, 148 Tianmushan Road, Hangzhou, China Postal code：310028
Tel：+86-571-88273162 Email：fitee@zju.edu.cn
It is recommended to read the content of this site in Chrome&IE9+. Please switch to extreme mode in browser 360.
Cookies We use cookies to help provide and enhance our service and tailor content. By continuing, you agree to the use of cookies.

⁰