This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Triggered Message Sequence Charts
August 2006 (vol. 32 no. 8)
pp. 587-607
This paper introduces Triggered Message Sequence Charts (TMSCs), a graphical, mathematically well-founded framework for capturing scenario-based system requirements of distributed systems. Like Message Sequence Charts (MSCs), TMSCs are graphical depictions of scenarios, or exchanges of messages between processes in a distributed system. Unlike MSCs, however, TMSCs are equipped with a notion of trigger that permits requirements to be made conditional, a notion of partiality indicating that a scenario may be subsequently extended, and a notion of refinement for assessing whether or not a more detailed specification correctly elaborates on a less detailed one. The TMSC notation also includes a collection of composition operators allowing structure to be introduced into scenario specifications so that interactions among different scenarios may be studied. In the first part of this paper, TMSCs are introduced and their use in support of requirements modeling is illustrated via two extended examples. The second part develops the mathematical underpinnings of the language.

[1] “Center-Tracon Automation System (CTAS) for Air Traffic Control,” http:/ctas.arc.nasa.gov/, 2006.
[2] “Integrated Medical Systems Inc.-lstat,” http://www.lstat.comlstat.html, 2006.
[3] “Message Sequence Charts (MSC),” ITU-TS Recommendation Z.120, 1996.
[4] T. Alspaugh and A. Antón, “Scenario Networks: A Case Study of the Enhanced Messaging System,” Proc. Seventh Int'l Workshop Requirements Eng.: Foundation for Software Quality, 2001.
[5] R. Alur and M. Yannakakis, “Model Checking of Message Sequence Charts,” Proc. 10th Int'l Conf. Concurrency Theory, pp.82-97, 1999.
[6] B. Genest, M. Minea, A. Muscholl, and D. Peled, “Specifying and Verifying Partial Order Properties Using Template MSCS,” Proc. Int'l Conf. Foundations of Software Science and Computation Structures, pp. 195-210, 2004.
[7] G. Booch, I. Jacobson, and J. Rumbaugh, The Unified Modeling Language User Guide, 1999.
[8] B. Sengupta, “Triggered Message Sequence Charts,” PhD thesis, State Univ. of New York (SUNY) Stony Brook, 2003.
[9] B. Sengupta and R. Cleaveland, “Triggered Message Sequence Charts,” Proc. ACM SIGSOFT 2002 (FSE-10), pp. 167-176, 2002.
[10] B. Sengupta and R. Cleaveland, “Refinement-Based Requirements Modeling Using Triggered Message Sequence Charts,” Proc. IEEE Int'l Requirements Eng. Conf., 2003.
[11] B. Sengupta and R. Cleaveland, “Towards Formal but Flexible Scenarios,” Proc. Second Int'l Workshop Scenarios and State Machines: Models, Algorithms and Tools, 2003.
[12] B. Sengupta and R. Cleaveland, “TRIM: A Tool for Triggered Message Sequence Charts,” Proc. 15th Computer Aided Verification Conf. (CAV '03), 2003.
[13] B. Sengupta and R. Cleaveland, “Executable Requirements Specifications Using Triggered Message Sequence Charts,” Proc. Second Int'l Conf. Distributed Computing and Internet Technology (ICDCIT), 2005.
[14] B. Sengupta and R. Cleaveland, “An Integrated Framework for Scenarios And State-Machines,” Proc. Fifth Int'l Conf. Integrated Formal Methods (IFM), pp. 366-385, 2005.
[15] R. Cleaveland and M.C.B. Hennessy, “Testing Equivalence as a Bisimulation Equivalence,” Formal Aspects of Computing, vol. 5, pp.1-20, 1993.
[16] R. Cleaveland, J. Parrow, and B. Steffen, “The Concurrency Workbench: A Semantics Based Tool for the Verification of Concurrent Systems,” ACM Trans. Programming Languages and Systems, vol. 15, no. 1, 1993.
[17] R. Cleaveland and S. Sims, “Generic Tools for Verifying Concurrent Systems,” Science of Computer Programming, vol. 42, no. 1, pp. 39-47, Jan. 2002.
[18] C. Rolland and C. Ben Achour, “Guiding the Construction of Textual Use Case Specifications,” Data and Knowledge Eng. J., vol. 25, nos. 1-2, pp. 125-160, 1998.
[19] C. Rolland, C. Souveyet, and C. Ben Achour, “Guiding Goal Modeling Using Scenarios,” IEEE Trans. Software Eng., vol. 24, no. 12, 1998.
[20] C. Rolland et al., “A proposal for a Scenario Classification Framework,” Requirements Eng. J., vol. 3, no. 1, pp. 23-47, 1998.
[21] W. Damm and D. Harel, “LSCs: Breathing Life into Message Sequence Charts,” Formal Methods in System Design, vol. 19, no. 1, 2001.
[22] R. De Nicola and M.C.B. Hennessy, “Testing Equivalences for Processes,” Theoretical Computer Science, vol. 34, pp. 83-133, 1983.
[23] D. Harel, “Statecharts: A Visual Formalism for Complex Systems,” Science of Computer Programming, vol. 8, pp. 231-274, 1987.
[24] J.C.S. do Prado Leite et al., “Enhancing a Requirements Baseline with Scenarios,” Proc. Third IEEE Int'l Symp. Requirements Eng., 1997.
[25] E. Gunter, A. Muscholl, and D. Peled, “Compositional Message Sequence Charts,” Proc. Tools and Algorithms for Construction and Analysis of Systems (TACAS), pp. 496-511, 2001.
[26] J. Grabowski, P. Graubmann, and E. Rudolph, “Towards a Petri Net Based Semantics for Message Sequence Charts,” Proc. Sixth SDL Forum, Using Objects, pp. 179-190, 1993.
[27] M. Hennessy, Algebraic Theory of Processes. The MIT Press, 1988.
[28] H. Kugler, D. Harel, A. Pnueli, Y. Lu, and Y. Bontemps, “Temporal Logic for Scenario-Based Specifications,” Proc. Tools and Algorithms for Construction and Analysis of Systems (TACAS), 2005.
[29] C.A.R. Hoare, Communicating Sequential Processes. London: Prentice-Hall, 1985.
[30] I. Jacobson, “The Use Case Construct in Object-Oriented Software Engineering,” Scenario-Based Design: Envisioning Work and Technology in System Development, pp. 309-336, 1995.
[31] ITU-T, “Recommendation z.100: Specification and Description Language (SSL),” 1994.
[32] I. Kruger, “Distributed System Design with Message Sequence Charts,” PhD thesis, Technical Univ. of Munich, 2000.
[33] P.B. Ladkin and S. Leue, “Interpreting Message Flow Graphs,” Formal Aspects of Computing, vol. 7, no. 5, pp. 473-509, 1995.
[34] M. Main, “Trace, Failure and Testing Equivalences for Communicating Processes,” Int'l J. Parallel Processing, vol. 16, no. 5, pp.383-400, 1987.
[35] S. Mauw and M. Reniers, “Refinement in Interworkings,” Proc. Int'l Conf. Concurrency Theory (CONCUR '96), U. Montanari and V.Sassone, eds., pp. 671-686, Aug. 1996.
[36] S. Mauw and M.A. Reniers, “An Algebraic Semantics of Basic Message Sequence Charts,” The Computer J., vol. 37, no. 4, pp. 269-277, 1994.
[37] R. Milner, Communication and Concurrency. London: Prentice-Hall, 1989.
[38] N. Maiden, S. Minocha, K. Manning, and M. Ryan, “CREWS-SAVRE: Systematic Scenario Generation and Use,” Proc. Int'l Conf. Requirements Eng., pp. 148-155, 1998.
[39] W. Reisig, Petri Nets: An Introduction, vol. 4 of EATCS Monographs in Theoretical Computer Science, 1985.
[40] M.A. Reniers, “Message Sequence Chart: Syntax and Semantics,” PhD thesis, Eindhoven Univ. of Tech nology, 1999.
[41] S. Uchitel, J. Kramer, and J. Magee, “Negative Scenarios for Implied Scenario Elicitation,” Proc. ACM SIGSOFT 2002 (FSE-10), 2002.
[42] J. Kramer, S. Uchitel, and J. Magee, “Synthesis of Behavioral Models from Scenarios,” IEEE Trans. Software Eng., vol. 29, no. 2, Feb. 2003.
[43] T. Alspaugh, A. Antón, T. Barnes, and B. Mott, “An Integrated Scenario Management Strategy,” Proc. IEEE Int'l Symp. Requirements Eng., pp. 142-149, 1999.

Index Terms:
Message Sequence Charts, scenarios, requirements modeling, formal semantics, refinement.
Citation:
Bikram Sengupta, Rance Cleaveland, "Triggered Message Sequence Charts," IEEE Transactions on Software Engineering, vol. 32, no. 8, pp. 587-607, Aug. 2006, doi:10.1109/TSE.2006.82
Usage of this product signifies your acceptance of the Terms of Use.