UML状态图的机械语义和精化研究

盛枫; 窦亮; 杨宗源

doi:10.1631/FITEE.1601196

Your Location：

Home >

Browse articles >

UML状态图的机械语义和精化研究

常规文章 | Updated：2022-05-19

- UML状态图的机械语义和精化研究
- Mechanized semantics and refinement of UML-Statecharts
- 信息与电子工程前沿（英文） 2017年18卷第11期页码：1773-1783
- 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：
  
  Project supported by the National Natural Science Foundation of China (No. 61070226)
- DOI：10.1631/FITEE.1601196
  中图分类号： TP311.5
- 收稿：2016-04-24，
  
  修回：2017-11-29，
  
  纸质出版：2017-11
- Accepted：
Scan QR Code
盛枫, 窦亮, 杨宗源. UML状态图的机械语义和精化研究[J]. 信息与电子工程前沿（英文）, 2017,18(11):1773-1783.

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.
盛枫, 窦亮, 杨宗源. UML状态图的机械语义和精化研究[J]. 信息与电子工程前沿（英文）, 2017,18(11):1773-1783. DOI： 10.1631/FITEE.1601196.

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

浏览量

Downloads

CSCD

文章被引用时，请邮件提醒。

Submit

工具集

关联资源

暂无数据