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.
@conference(L-TPTS-02-TimedMSCs,
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)},
year=2002,
series={ENTCS},
volume={65.6},
editor={Eugene Asarin and Oded Maler and Sergio Yovine},
publisher={Elsevier},
month={April}
)
Valid XHTML 1.0 Strict, valid CSS.
Author: Philipp Lucas.