Abstract
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.
Original language | English |
---|---|
Title of host publication | Proceedings of the First International Workshop on Scenarios and State Machines (SCESM), (ICSE'02 workshop) |
Editors | Tarja Systa, Albert Zundorf |
Publication status | Published - 2002 |
Keywords
- Automata
- Live Sequence Charts
- Scenario
- LSCs
- Reactive System
- Synthesis