模态顺序图uMSD 的形式语义

doi:10.3724/SP.J.1001.2011.03776

微信服务号

微信订阅号

2025年4月4日 4:34 星期五

首页 > 过刊浏览>2011年第22卷第4期 >659-675. DOI:10.3724/SP.J.1001.2011.03776

PDF HTML阅读 XML下载导出引用引用提醒

模态顺序图uMSD 的形式语义
DOI:
                        10.3724/SP.J.1001.2011.03776
                    
CSTR:
                        
                    
作者:
                        李雯睿李雯睿
河海大学 计算机及信息工程学院,江苏 南京 210098;南京晓庄学院 数学与信息技术学院,江苏 南京 211171;武汉大学 软件工程国家重点实验室,湖北 武汉 430072
在期刊界中查找
在百度中查找
在本站中查找
王志坚王志坚
河海大学 计算机及信息工程学院,江苏 南京 210098
在期刊界中查找
在百度中查找
在本站中查找
张鹏程张鹏程
河海大学 计算机及信息工程学院,江苏 南京 210098;武汉大学 软件工程国家重点实验室,湖北 武汉 430072
在期刊界中查找
在百度中查找
在本站中查找

                    
作者单位:
作者简介:
通讯作者:
中图分类号:
基金项目:国家高技术研究发展计划(863)(2007AA01Z178); 中央高校基本科研业务费专项资金(2009B04314); 武汉大学软件工程国家重点实验室开放基金(2010-08-01)

Formal Semantics of Universal Modal Sequence Diagram

Author:

LI Wen-Rui
LI Wen-Rui
College of Computer and Information Engineering, Hohai University, Nanjing 210098, China;School of Mathematics and Information Technology, Nanjing Xiaozhuang University, Nanjing 211171, China;State Key Laboratory of Software Engineering, Wuhan University, Wuhan 430072, China
在期刊界中查找
在百度中查找
在本站中查找
WANG Zhi-Jian
WANG Zhi-Jian
College of Computer and Information Engineering, Hohai University, Nanjing 210098, China
在期刊界中查找
在百度中查找
在本站中查找
ZHANG Peng-Cheng
ZHANG Peng-Cheng
College of Computer and Information Engineering, Hohai University, Nanjing 210098, China;State Key Laboratory of Software Engineering, Wuhan University, Wuhan 430072, China
在期刊界中查找
在百度中查找
在本站中查找

Affiliation:

Fund Project:

摘要

图/表

访问统计

参考文献 [14]

相似文献 [20]

引证文献

资源附件

文章评论

摘要:

UML 2.0 顺序图已广泛应用于业界,但其语义模糊,以至于不能有效地加以使用.模态顺序图(modal sequence diagram,简称MSD)是对UML 2.0 顺序图的模态扩展,区分了强制场景(用universal MSD 表示,简称uMSD)和可能场景(用existential MSD 表示,简称eMSD).其中,uMSD 具有较强的表达能力,能够用于表示并发系统的时态性质,故主要工作围绕uMSD 展开.为了使uMSD 用于形式化分析、验证和监控,给出基于自动机的uMSD 语义解释,并给出各种操作符的算法,用性质规约模式度量uMSD 的表达能力.最后进行了实例研究,并讨论了其应用前景.

关键词:模态顺序图;弱交换Büchi 自动机;性质规约模式

Abstract:

The UML 2.0 Sequence Diagram has been extensively applied in industry. However, the vague semantics of UML 2.0 Sequence Diagram prevent it from being applied effectively. Modal Sequence Diagram is the modal extension of UML 2.0 Sequence Diagram, which distinguishes mandatory scenarios (described by universal MSD, denoted as uMSD) from possible scenarios (described by existential MSD, denoted as eMSD). uMSD is more expressive than eMSD and can represent the temporal properties of concurrent systems. Therefore, the main work of the paper is on uMSD. In order to make uMSD extensively used for formal analysis, verification, and monitoring, the formal semantics of uMSD, based on the Weak Alternating Büchi automaton, are represented, and the transformation algorithms of various operators are given in detail. Next, the expressiveness of uMSD is measured by the well known property specification patterns. Finally, an example is studied, and its future applications are discussed.

Key words:modal sequence diagram; linear weak alternating Büchi automaton; property specification pattern

参考文献

[1] ITU-T. Recommendation Z. 120: Message Sequence Charts. Geneva: ITU-T, 1999.

[2] Damm W, Harel D. LSCs: Breathing life into message sequence charts. Formal Methods in System Design, 2001,19(1):45?80. [doi: 10.1023/A:1011227529550]

[3] Object Management Group (OMG). UML: Superstructure Version 2.2. 2009.

[4] Harel D, Maoz S. Assert and negate revisited: Modal semantics for UML sequence diagrams. Software and Systems Modeling, 2008,7(2):237?252. [doi: 10.1007/s10270-007-0054-z]

[5] Kupferman O, Vardi M. Weak alternating automata are not that weak. ACM Trans. on Computational Logic, 2001,2(3):408?429. [doi: 10.1145/377978.377993]

[6] Dwyer MB, Avrunin GS, Corbett JC. Patterns in property specifications for finite-state verification. In: Boehm B, Garlan D, Kramer J, eds. Proc. of the 21th Int’l Conf. on Software Engineering. CA: IEEE Press, 1999. 411?431. [doi: 10.1145/302405.302672]

[7] Sengupta B, Cleaveland R. Triggered message sequence charts. IEEE Trans. on Software Engineering, 2006,32(8):587?607. [doi: 10.1109/TSE.2006.82]

[8] Klose J, Wittke H. An automata based interpretation of live sequence charts. In: Margaria T, Yi W, eds. Proc. of the ETAPS 2001 and TACAS 2001. LNCS 2031, Heidelberg: Springer-Verlag, 2001. 512?527. [doi: 10.1007/3-540-45319-9_35]

[9] Zanolin L, Ghezzi C, Baresi L. An approach to model and validate publish/subscribe architectures. In: Edwards SH, ed. Proc. of the SAVCBS 2003 Workshop at ESEC/FSE. Ames, 2003. 35?41.

[10] Haugen ?, Husa KE, Runde RK, St?len K. STAIRS towards formal design with sequence diagrams. Software and Systems Modeling, 2005,4(4):355?367. [doi: 10.1007/s10270-005-0087-0]

[11] Autili M, Inverardi P, Pelliccione P. A scenario based notation for specifying temporal properties. In: Proc. of the 5th Int’l Workshop on Scenarios and State Machines: Models, Algorithms and Tools. 2006. 21?28. [doi: 10.1145/1138953.1138959]

[12] Zhang PC, Zhou Y, Li B X, Xu BW. Property sequence charts: Formal syntax and semantic. Journal of Computer Research and Development, 2008,45(2):318?328 (in Chinese with English abstract).

[13] Zhang PC, Li BX, Li WR. Syntax and semantics of timed property sequence chart. Journal of Software, 2010,21(11):2752?2767 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/3711.htm [doi: 10.3724/SP.J.1001.2010.03711]

[14] Li WR, Wang ZJ. Monitoring composite services with universal modal sequence diagrams. In: Proc. of the 16th Asia-Specific Software Engineering Conf. (APESC 2009). Penang: IEEE Computer Society Press, 2009. 69?76. [doi: 10.1109/APSEC.2009.65]

引用本文

李雯睿,王志坚,张鹏程.模态顺序图uMSD 的形式语义.软件学报,2011,22(4):659-675

复制

文章指标

点击次数:6643
下载次数: 7201
HTML阅读次数: 0
引用次数: 0

历史

收稿日期:2009-03-25
最后修改日期:2009-10-23
录用日期:
在线发布日期:
出版日期:

微信服务号

微信订阅号

引用本文

分享

文章指标

历史

文章二维码

微信服务号

微信订阅号

引用本文

分享

微信扫一扫：分享

文章指标

历史

文章二维码