Model Checking Combined Fragments of Sequence Diagrams

作者: Hui Shen , Mark Robinson , Jianwei Niu

DOI: 10.1007/978-3-642-45404-2_7

关键词:

摘要: Graphical representations of scenarios using the Combined Fragments UML Sequence Diagrams, serve as a well-accepted means for expressing an aggregation multiple traces encompassing complex and concurrent behaviors. However, increase difficulty analysis scenarios. This paper introduces approach to formally verify all Fragments, nested model checking.

参考文章(26)
Doron Peled, Specification and Verification of Message Sequence Charts IFIP Advances in Information and Communication Technology. pp. 139- 154 ,(2000) , 10.1007/978-0-387-35533-7_9
Christoph Eichner, Hans Fleischhack, Roland Meyer, Ulrik Schrimpf, Christian Stehno, Compositional semantics for UML 2.0 sequence diagrams using petri nets Lecture Notes in Computer Science. pp. 133- 148 ,(2005) , 10.1007/11506843_9
Anca Muscholl, Doron Peled, Deciding Properties of Message Sequence Charts Scenarios: Models, Transformations and Tools. pp. 43- 65 ,(2005) , 10.1007/11495628_3
Rajeev Alur, Kousha Etessami, P. Madhusudan, A Temporal Logic of Nested Calls and Returns tools and algorithms for construction and analysis of systems. ,vol. 2988, pp. 467- 481 ,(2004) , 10.1007/978-3-540-24730-2_35
Hillel Kugler, David Harel, Amir Pnueli, Yuan Lu, Yves Bontemps, Temporal Logic for Scenario-Based Specifications Tools and Algorithms for the Construction and Analysis of Systems. ,vol. 3440, pp. 445- 460 ,(2005) , 10.1007/978-3-540-31980-1_29
Stefan Leue, Peter B. Ladkin, Implementing and Verifying MSC Specifications Using Promela/XSpin DIMACS. ,(1997)
Rajeev Alur, Mihalis Yannakakis, Model Checking of Message Sequence Charts CONCUR’99 Concurrency Theory. pp. 114- 129 ,(1999) , 10.1007/3-540-48320-9_10
Elsa L. Gunter, Anca Muscholl, Doron A. Peled, Compositional Message Sequence Charts tools and algorithms for construction and analysis of systems. ,vol. 5, pp. 496- 511 ,(2001) , 10.1007/3-540-45319-9_34
Anca Muscholl, Doron Peled, Zhendong Su, Deciding Properties for Message Sequence Charts foundations of software science and computation structure. pp. 226- 242 ,(1998) , 10.1007/BFB0053553
Alexander Knapp, Jochen Wuttke, Model checking of UML 2.0 interactions model driven engineering languages and systems. pp. 42- 51 ,(2006) , 10.5555/1762828.1762836