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.

Selected Related Publications

• R. Jonk, J. Voeten, M. Geilen, T. Basten, and R. Schiffelers, “Smt-based verification of temporal properties for component-based software systems,” Ifac-papersonline, vol. 53, iss. 4, pp. 493-500, 2020.
  [Bibtex]

  @article{JVGBS20,
  title = {SMT-based verification of temporal properties for component-based software systems},
  journal = {IFAC-PapersOnLine},
  volume = {53},
  number = {4},
  pages = {493-500},
  year = {2020},
  note = {15th IFAC Workshop on Discrete Event Systems WODES 2020 — Rio de Janeiro, Brazil, 11-13 November 2020},
  issn = {2405-8963},
  doi = {https://doi.org/10.1016/j.ifacol.2021.04.045},
  url = {https://www.sciencedirect.com/science/article/pii/S2405896321000951},
  author = {R. Jonk and J. Voeten and M. Geilen and T. Basten and R. Schiffelers},
  keywords = {Verification, Component-based software system, Message Sequence Chart, Metric Temporal Logic, Modeling}
  }

• B. Hooimeijer, “Model inference for legacy software in component-based architectures,” , 2020.
  [Bibtex]

  @@mastersthesis{Hooi20,
  title={Model inference for legacy software in component-based architectures},
  author={Hooimeijer, B},
  year={2020},
  school={Master’s thesis, Eindhoven University of Technology}
  }

• R. Jonk, J. Voeten, M. Geilen, R. Theunissen, Y. Blankenstein, T. Basten, and R. Schiffelers, “Inferring timed message sequence charts from execution traces of large-scale component-based software systems,” , 2019.
  [Bibtex]

  @article{JVGea19,
  title={Inferring Timed Message Sequence Charts from Execution Traces of Large-scale Component-based Software Systems},
  author={Jonk, Ruben and Voeten, Jeroen and Geilen, Marc and Theunissen, Rolf and Blankenstein, Yuri and Basten, Twan and Schiffelers, Ramon},
  year={2019}
  }

References

@article{HT03,
title={Message sequence charts},
author={Harel, David and Thiagarajan, PS},
journal={UML for real: design of embedded real-time systems},
pages={77--105},
year={2003},
publisher={Springer}
}

@article{AHP96,
title={An analyzer for message sequence charts},
author={Alur, Rajeev and Holzmann, Gerard and Peled, Doron},
journal={Lecture Notes in Computer Science},
volume={1055},
pages={35--48},
year={1996},
publisher={Berlin: Springer-Verlag, 1973-}
}

@article{JVGea19,
title={Inferring Timed Message Sequence Charts from Execution Traces of Large-scale Component-based Software Systems},
author={Jonk, Ruben and Voeten, Jeroen and Geilen, Marc and Theunissen, Rolf and Blankenstein, Yuri and Basten, Twan and Schiffelers, Ramon},
year={2019}
}

@@mastersthesis{Hooi20,
title={Model inference for legacy software in component-based architectures},
author={Hooimeijer, B},
year={2020},
school={Master’s thesis, Eindhoven University of Technology}
}

[5] R. Jonk, J. Voeten, M. Geilen, T. Basten, and R. Schiffelers, “Smt-based verification of temporal properties for component-based software systems,” Ifac-papersonline, vol. 53, iss. 4, pp. 493-500, 2020.
[Bibtex]

@article{JVGBS20,
title = {SMT-based verification of temporal properties for component-based software systems},
journal = {IFAC-PapersOnLine},
volume = {53},
number = {4},
pages = {493-500},
year = {2020},
note = {15th IFAC Workshop on Discrete Event Systems WODES 2020 — Rio de Janeiro, Brazil, 11-13 November 2020},
issn = {2405-8963},
doi = {https://doi.org/10.1016/j.ifacol.2021.04.045},
url = {https://www.sciencedirect.com/science/article/pii/S2405896321000951},
author = {R. Jonk and J. Voeten and M. Geilen and T. Basten and R. Schiffelers},
keywords = {Verification, Component-based software system, Message Sequence Chart, Metric Temporal Logic, Modeling}
}

[6] M. Hendriks and F. W. Vaandrager, “Reconstructing critical paths from execution traces,” in 2012 ieee 15th international conference on computational science and engineering, 2012, pp. 524-531.
[Bibtex]

@INPROCEEDINGS{HV12,
author={Hendriks, Martijn and Vaandrager, Frits W.},
booktitle={2012 IEEE 15th International Conference on Computational Science and Engineering},
title={Reconstructing Critical Paths from Execution Traces},
year={2012},
volume={},
number={},
pages={524-531},
doi={10.1109/ICCSE.2012.78}
}