Triggered message sequence charts

Abstract

We propose an extension to Message Sequence Charts called Triggered Message Sequence Charts (TMSCs) that are intended to capture system specifications involving nondeterminism in the form of conditional scenarios. The visual syntax of TMSCs closely resembles that of MSCs; the semantics allows us to translate a TMSC specification into a framework that supports a notion of refinement based on Denicola's and Hennessy's must preorder. A simple but non-trivial example illustrates the utility of our extension to MSCs.

BibTeX

@inproceedings{Sengupta-Cleaveland:FSE02,
  author    = {Bikram Sengupta and
               Rance Cleaveland},
  title     = {Triggered message sequence charts},
  booktitle = {FSE},
  pages     = {167--176},
  publisher = {{ACM}},
  year      = {2002},
}

Triggered message sequence charts

Abstract

Related papers