Message Sequence Charts (MSCs) are a widely used scenario notation. However, we believe that this language lacks message abstraction and the ability to express whether a scenario is an example or a universal rule. Live Sequence Charts (LSCs) improve MSCs by solving these two shortcomings. However, LSCs have no formally defined high-level structuring mechanism. We extend LSCs with composition operators and define their semantics in terms of $\omega$-regular traces. We build Buchi automata from these scenarios. We show that standard algorithms on this (low-level) formalism can be used to check consistency and refinement, and to synthesize a state-based specification from a set of consistent requirements.
|titre||Proceedings of the First International Workshop on Scenarios and State Machines (SCESM), (ICSE'02 workshop)|
|rédacteurs en chef||Tarja Systa, Albert Zundorf|
|Etat de la publication||Publié - 2002|