Live sequence charts: An introduction to lines, arrows, and strange boxes in the context of formal verification

Abstract

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. © Springer-Verlag Berlin Heidelberg 2004.