Timed Semantics of Message Sequence Charts Based on Timed Automata


Message Sequence Charts (MSCs) provide a way for quick and easily understandable modeling of concurrent systems. Apart from their intuitive semantics easily deduced from their visual syntax, there is a formally defined semantics---Unfortunately, the semantics intuitively assigned to them is sometimes at odds with the formal semantics. In this paper, we will show an alternative approach to the semantics of MSCs, which will enable us to formally model their timed behaviour. Furthermore, we show how some generalisations of ordering events can lead to a language better suited to model real-world requirements. To ease the task of analyzing (High-Level) MSCs, we identify a subclass of those which can be translated into finite (timed or untimed) automata and specify the translation, thus laying the foundation for model checking.

Download paper (PDF)

BibTeX information

 author={Philipp Lucas},
 title={Timed Semantics of Message Sequence Charts Based on Timed Automata},
 booktitle={Proceedings of the Workshop of Theory and Practice of
  Timed Systems (TPTS'02)},
 editor={Eugene Asarin and Oded Maler and Sergio Yovine},

back to publications

Valid XHTML 1.0 Strict, valid CSS.

Best viewed with any browser.

Author: Philipp Lucas.