Live Sequence Charts: An Introduction to Lines, Arrows, and Strange Boxes in the Context of Formal Verification

  • Brill M
  • Damm W
  • Klose J
 et al. 
  • 5


    Mendeley users who have this article in their library.
  • 19


    Citations of this article.


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 verifica- tion, serious deficiencies emerge: MSCs do not provide means to distin- guish 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 be- tween 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. u

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • Matthias Brill

  • Werner Damm

  • Jochen Klose

  • Bernd Westphal

  • Hartmut Wittke

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free