Timed Message Sequence Charts

Message Sequence Charts (MSC) ^[1] are a standardized model to capture interaction in the form of message exchanges between concurrent components. They are defined (among others) in UML. It can be used as a specification of desired behavior, or it may be used to capture actual behavior observed in a real system.

The underlying mathematical model considers a set of events with a partial order relation that captures all specified or observed dependencies. All events of a single component are sequential, totally ordered and the message exchanges between components establish ordering relations between event on different components.

Time Message Sequence Charts ^[2] are an extension of message sequence charts that include quantitative time. Different flavors exist. One example is the annotation of dependencies with a minimal or actual time difference between events. When event are observed on different components this may require some form of time synchronization between distributed components.

When MSCs are used to represent actual, observed behavior in a system, an effective inference method is required ^[3][4]. Software or hardware needs to be instrumented to extract the relevant dat and a model is constructed from that data that represents the observed behavior.

Subsequently inferred models can be used for different kinds of analysis, for example, verification of timing properties ^[5], critical path analysis ^[6], or root-cause analysis.

References

1. David Harel and PS Thiagarajan (2003): Message sequence charts. In: UML for real: design of embedded real-time systems, pp. 77–105, 2003.
2. Rajeev Alur and Gerard Holzmann and Doron Peled (1996): An analyzer for message sequence charts. In: Lecture Notes in Computer Science, vol. 1055, pp. 35–48, 1996.
3. Ruben Jonk and Jeroen Voeten and Marc Geilen and Rolf Theunissen and Yuri Blankenstein and Twan Basten and Ramon Schiffelers (2019): Inferring Timed Message Sequence Charts from Execution Traces of Large-scale Component-based Software Systems. In: 2019.
4. B Hooimeijer (2020): Model inference for legacy software in component-based architectures. Master’s thesis, Eindhoven University of Technology, 2020.
5. R. Jonk and J. Voeten and M. Geilen and T. Basten and R. Schiffelers (2020): SMT-based verification of temporal properties for component-based software systems. In: IFAC-PapersOnLine, vol. 53, no. 4, pp. 493-500, 2020, ISSN: 2405-8963, (15th IFAC Workshop on Discrete Event Systems WODES 2020 — Rio de Janeiro, Brazil, 11-13 November 2020).
6. Martijn Hendriks and Frits W. Vaandrager (2012): Reconstructing Critical Paths from Execution Traces. In: 2012 IEEE 15th International Conference on Computational Science and Engineering, pp. 524-531, 2012.

Selected Related Publications

@bachelorthesis{Hooi20,

title = {Model inference for legacy software in component-based architectures},

author = {B Hooimeijer},

year  = {2020},

date = {2020-01-01},

urldate = {2020-01-01},

school = {Master’s thesis, Eindhoven University of Technology},

keywords = {},

pubstate = {published},

tppubtype = {bachelorthesis}

}

@article{JVGea19,

title = {Inferring Timed Message Sequence Charts from Execution Traces of Large-scale Component-based Software Systems},

author = {Ruben Jonk and Jeroen Voeten and Marc Geilen and Rolf Theunissen and Yuri Blankenstein and Twan Basten and Ramon Schiffelers},

year  = {2019},

date = {2019-01-01},

urldate = {2019-01-01},

keywords = {},

pubstate = {published},

tppubtype = {article}

}

@inproceedings{HV12,

title = {Reconstructing Critical Paths from Execution Traces},

author = {Martijn Hendriks and Frits W. Vaandrager},

doi = {10.1109/ICCSE.2012.78},

year  = {2012},

date = {2012-01-01},

urldate = {2012-01-01},

booktitle = {2012 IEEE 15th International Conference on Computational Science and Engineering},

pages = {524-531},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@article{HT03,

title = {Message sequence charts},

author = {David Harel and PS Thiagarajan},

year  = {2003},

date = {2003-01-01},

urldate = {2003-01-01},

journal = {UML for real: design of embedded real-time systems},

pages = {77–105},

publisher = {Springer},

keywords = {},

pubstate = {published},

tppubtype = {article}

}

@article{AHP96,

title = {An analyzer for message sequence charts},

author = {Rajeev Alur and Gerard Holzmann and Doron Peled},

year  = {1996},

date = {1996-01-01},

urldate = {1996-01-01},

journal = {Lecture Notes in Computer Science},

volume = {1055},

pages = {35–48},

publisher = {Berlin: Springer-Verlag, 1973-},

keywords = {},

pubstate = {published},

tppubtype = {article}

}