微信服务号

微信订阅号

2025-4-6- 4
Home > Archive>Volume 22, Issue 4, 2011 >659-675. DOI:10.3724/SP.J.1001.2011.03776
PDF HTML XML Export Cite reminder
Formal Semantics of Universal Modal Sequence Diagram
Author:
Affiliation:

  • Article
    • | |
  • Metrics
    • |
  • Reference [14]
    • |
  • Related
    • |
  • Cited by [2]
    • | |
  • Comments
    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.

    Reference
    [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]
    Related
    Comments
    Comments
    分享到微博
    Submit
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:March 25,2009
  • Revised:October 23,2009
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2033288Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063