The Community for Technology Leaders
RSS Icon
Issue No.03 - May/June (2008 vol.34)
pp: 305-320
Bill Mitchell , University of Surrey, Guilford
UML sequence diagrams (SDs) are a mainstay of requirements specifications for communication protocols. Mauw and Reniers' algebraic (MRA) semantics formally specifies a behaviour for these SDs that guarantees deadlock free processes. Practitioners commonly use communication semantics that differ from MRA, which may result in deadlocks. For example FIFO, token ring, etc. We define a process algebra that is an extension of the MRA semantics for regular sequence diagrams. Our algebra can describe several commonly used communication semantics. Regular SDs are constructed from concurrent message flows via iteration, branching, and sequential composition. Their behaviour is defined in terms of a set of partial orders on the events in the SD. Such partial orders are known as causal orders. We define partial order theoretic properties of a causal order that are particular kinds of race condition. We prove any of the common communication semantics we list either guarantees deadlock free SDs or can result in a deadlock if and only if a causal order of an SD contains one of these types of race condition. This describes a complete classification of deadlocks as specific types of race condition.
Requirements Analysis, Formal methods, Distributed programming, Distributed networks, Protocol verification
Bill Mitchell, "Characterizing Communication Channel Deadlocks in Sequence Diagrams", IEEE Transactions on Software Engineering, vol.34, no. 3, pp. 305-320, May/June 2008, doi:10.1109/TSE.2008.28
[1] R. Alur and M. Yannakakis, “Model Checking of Message Sequence Charts,” Proc. 10th Int'l Conf. Concurrency Theory, pp.114-129, 1999.
[2] R. Alur, K. Etessami, and M. Yannakakis, “Inference of Message Sequence Charts,” Proc. 22nd Int'l Conf. Software Eng., pp. 304-313, 2000.
[3] R. Alur, K. Etessami, and M. Yannakakis, “Realizability and Verification of MSC Graphs,” Proc. 28th Int'l Colloquium Automata, Languages, and Programming, pp. 797-808, 2001.
[4] D. Amyot and A. Eberlein, “An Evaluation of Scenario Notations and Construction Approaches for Telecommunication Systems Development,” Telecomm. Systems, vol. 24, no. 1, pp. 61-94, 2003.
[5] P. Baker, P. Bristow, S. Burton, D. King, C. Jervis, B. Mitchell, and R. Thomson, “Detecting and Resolving Semantic Pathologies in UML Sequence Diagrams,” Proc. Joint 10th European Software Eng. Conf. and 13th ACM SIGSOFT Symp. Foundations of Software Eng., pp. 50-59, 2005.
[6] P. Baker, P. Bristow, C. Jervis, D. King, and B. Mitchell, “Automatic Generation of Conformance Tests from Message Sequence Charts,” Proc. Third Sensor Array and Multichannel Signal Processing Workshop, Telecomm. and Beyond: The Broader Applicability of MSC and SDL, pp. 170-198, 2004.
[7] H. Ben-Abdhallah and S. Leue, “Syntactic Detection of Process Divergence and Non-Local Choice in Message Sequence Charts,” Proc. Third Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 259-274, 1997.
[8] M. Beyer, W. Dulz, and F. Zhen, “Automated TTCN-3 Test Case Generation by Means of UML Sequence Diagrams and Markov Chains,” Proc. 12th Asian Test Symp., pp. 102-106, 2003.
[9] Y. Bontemps and P.-Y. Schobbens, “Synthesis of Open Reactive Systems from Scenario-Based Specifications,” Proc. Third Int'l Conf. Application of Concurrency to System Design, pp. 41-50, 2003.
[10] Y. Bontemps and P. Heymens, “Turning High-Level Live Sequence Charts into Automata,” Proc. 24th Int'l Conf. Software Eng. Scenarios and State Machines: Models Algorithms and Tools Workshop, May 2002.
[11] S. Chung, H.S. Kim, H.S. Bae, Y.R. Kwon, and B.S. Lee, “Testing of Concurrent Programs Based on Message Sequence Charts,” Proc. Int'l Symp. Software Eng. for Parallel and Distributed Systems, pp. 72-82, 1999.
[12] “Methodological Approach to the Use of Object-Orientation in the Standards Making Process,” ETSI EG 201 872, 2001.
[13] “Guidelines for the Use of Formal SDL as a Descriptive Tool,” ETSI EG 202 106, 2003.
[14] T. Gehrke, M. Hilhn, and H. Wehrkeim, “An Algebraic Semantics for Message Sequence Chart Documents,” Proc. IFIP TC6 WG6.1 Joint Int'l Conf. Formal Description Techniques for Distributed Systems and Comm. Protocols and Protocol Specification, Testing and Verification, pp. 3-18, 1998.
[15] E. Gunter, A. Muscholl, and D. Peled, “Compositional Message Sequence Charts,” Proc. Seventh Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 496-511, 2001.
[16] G.J. Holzmann, D.A. Peled, and M.H. Redberg, “An Analyzer for Message Sequence Charts,” Software Concepts and Tools, vol. 17, no. 2, pp. 70-77, 1996.
[17] D. Harel and W. Damm, “LSCs: Breathing Life into Message Sequence Charts,” Formal Methods in System Design, vol. 19, pp. 45-80, 2001.
[18] D. Harel and H. Kugler, “Synthesizing State-Based Object Systems from LSC Specifications,” Int'l J. Foundations of Computer Science, vol. 13, no. 1, pp. 5-51, 2002.
[19] D. Harel, H. Kugler, and A. Pnueli, “Synthesis Revisited: Generating Statechart Models from Scenario-Based Requirements,” Formal Methods in Software and System Modeling, pp. 309-324, Springer, 2005.
[20] I. Kruger, R. Grosu, P. Scholz, and M. Broy, “From MSCs to Statecharts,” Proc. IFIP WG10.3/WG10.5 Int'l Workshop Distributed and Parallel Embedded Systems, pp. 61-71, 1998.
[21] S. Leue, L. Mehrmann, and M. Rezai, “Synthesizing Software Architecture Descriptions from Message Sequence Chart Specifications,” Proc. 13th IEEE Int'l Conf. Automated Software Eng., pp.192-195, 1998.
[22] M. Lohrey, “Safe Realizability of High-Level Message Sequence Charts,” Proc. 13th Int'l Conf. Concurrency Theory, pp. 177-192, 2002.
[23] S. Mauw and M.A. Reniers, “An Algebraic Semanitcs of Basic Message Sequence Charts,” Computer J., vol. 7, no. 5, pp. 473-509, 1995.
[24] S. Mauw and M.A. Reniers, “Operational Semantics for MSC'96,” Computer Networks, vol. 31, no. 17, pp. 1785-1799, 1999.
[25] B. Mitchell, “Resolving Race Conditions in Asynchronous Partial Order Scenarios,” IEEE Trans. Software Eng., vol. 31, no. 9, pp. 767-784, Sept. 2005.
[26] B. Mitchell, “Inherent Causal Orderings of Partial Order Scenarios,” Proc. Int'l Colloquium Theoretical Aspects of Computing, pp. 114-129, Sept. 2004.
[27] B. Mitchell, R. Thomson, and C. Jervis, Phase Automaton for Requirements Scenarios, Feature Interactions in Telecommunications and Software Systems VII, pp. 77-84. IOS Press, 2003.
[28] Object Management Group, “Unified Modeling Language Specification Version 2.0 Specification,” http:/, 2004.
[29] E. Rudolph, I. Schieferdecker, and J. Grabowski, Development of a MSC/UML Test Format. 153-164, Formale Beschreibungstechniken fur Verteilte Systeme, pp. 153-164. Verlag Shaker, 2000.
[30] A. Rountev and B. Connell, “Object Naming Analysis for Reverse-Engineered Sequence Diagrams,” Proc. 27th Int'l Conf. Software Eng., pp. 254-263, 2005.
[31] J. Schumann and J. Whittle, “Generating Statechart Designs from Scenarios,” Proc. 22nd Int'l Conf. Software Eng., pp. 314-323, 2000.
[32] J. Sun and J.S. Dong, “Synthesis of Distributed Processes from Scenario-Based Specifications,” Proc. Int'l Symp. Formal Methods, pp. 415-431, 2005.
[33] H.H. Wang, S. Qin, J. Sun, and J.S. Dong, “Realizing Live Sequence Charts in SystemVerilog,” Proc. First Joint IEEE/IFIP Symp. Theoretical Aspects of Software Eng., pp. 379-388, 2007.
[34] J. Whittle, J. Saboo, and R. Kwan, “From Scenarios to Code: An Air Traffic Control Case Study,” J. Software and Systems Modeling, vol. 4, no. 1, pp. 71-93, 2005.
[35] S. Uchitel, J. Kramer, and J. Magee, “Incremental Elaboration of Scenario-Based Specifications and Behaviour Models Using Implied Scenarios,” ACM Trans. Software Eng. and Methodology, vol. 13, no. 1, pp. 37-85, 2004.
[36] S. Uchitel, G. Brunet, and M. Chechik, “Behaviour Model Synthesis from Properties and Scenarios,” Proc. 29th Int'l Conf. Software Eng., pp. 34-43, 2007.
[37] Z.100 (11/99) ITU-T Recommendation—Languages for Telecommunications Applications—Specification and Description Language, 1999.
[38] MOST Dynamic Specification, Most Cooperation, SpecificationsMOST Specifications/, 2005.
[39] Z.120 (11/99) ITU-T Recommendation—Message Sequence Chart (MSC), 1999.
[40] ITU-T Recommendation Z.120 (04/1998) Annex B—Formal Semantics of Message Sequence Charts, 1998.
30 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool