Live Sequence Charts

An Introduction to Lines, Arrows, and Strange Boxes in the Context of Formal Verification
  • Matthias Brill
  • Werner Damm
  • Jochen Klose
  • Bernd Westphal
  • Hartmut Wittke
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3147)


The language of Message Sequence Charts (MSC) is a well-established visual formalism which is typically used to capture scenarios in the early stages of system development. But when it comes to rigorous requirements capturing, in particular in the context of formal verification, serious deficiencies emerge: MSCs do not provide means to distinguish mandatory and possible behavior, for example to demand that a communication is required to finally occur.

The Live Sequence Chart (LSC) language introduces the distinction between mandatory and possible on the level of the whole chart and for the elements messages, locations, and conditions. Furthermore they provide means to specify the desired activation time by an activation condition or by a whole communication sequence, called pre-chart.

We present the current stage of LSC language and a sketch of its formal semantics in terms of Timed Büchi Automata.


Formal Semantic Instantaneous Message Atomic Proposition Input Symbol Local Invariant 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    ITU-T: ITU-T Recommendation Z.120: Message Sequence Chart (MSC). ITU-T, Geneva (1993) Google Scholar
  2. 2.
    ITU-T: ITU-T Annex B to Recommendation Z.120: Algebraic Semantics of Message Sequence Charts. ITU-T, Geneva (1995) Google Scholar
  3. 3.
    Ben-Abdallah, H., Leue, S.: Expressing and analyzing timing constraints in message sequence chart specifications. Technical Report 97-04, Department of Electrical and Computer Engineering, University of Waterloo (1997) Google Scholar
  4. 4.
    Damm, W., Harel, D.: LSCs: Breathing life into message sequence charts. Formal Methods in System Design 19, 45–80 (2001)zbMATHCrossRefGoogle Scholar
  5. 5.
    Klose, J.: Live Sequence Charts: A Graphical Formalism for the Specification of Communication Behavior. PhD thesis, Carl von Ossietzky Universität Oldenburg (2003) Google Scholar
  6. 6.
    Lamport, L.: Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering 3 (1977)Google Scholar
  7. 7.
    Brill, M., Buschermöhle, R., Damm, W., Klose, J., Westphal, B., Wittke, H.: Formal verification of LSC’s in the development process. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 494–516. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  8. 8.
    Schlör, R.: Symbolic Timing Diagrams : A Visual Formalism for Model Verification. PhD thesis, Carl von Ossietzky Universität Oldenburg (2000) Google Scholar
  9. 9.
    Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science: Formal Models and Semantics, vol. B, Elsevier Science Publishers, Amsterdam (1990)Google Scholar
  10. 10.
    Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science: Formal Models and Semantics, vol. B, pp. 995–1072. Elsevier Science Publishers, Amsterdam (1990)Google Scholar
  11. 11.
    Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–236 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Harel, D., Marelly, R.: Come, Let’s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)Google Scholar
  13. 13.
    Harel, D., Kugler, H.: Synthesizing state-based object systems from LSC specifications. International Journal of Foundations of Computer Science 13, 5–51 (2002)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Matthias Brill
    • 1
  • Werner Damm
    • 1
  • Jochen Klose
    • 2
  • Bernd Westphal
    • 1
  • Hartmut Wittke
    • 3
  1. 1.Department für InformatikCarl von Ossietzky Universität OldenburgOldenburgGermany
  2. 2.Bombardier Transportation, BraunschweigBraunschweigGermany
  3. 3.OFFISOldenburgGermany

Personalised recommendations