Turning High-Level Live Sequence Charts into Automata

Yves Bontemps, Patrick Heymans

Research output: Contribution in Book/Catalog/Report/Conference proceedingConference contribution

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 languageEnglish
Title of host publicationProceedings of the First International Workshop on Scenarios and State Machines (SCESM), (ICSE'02 workshop)
EditorsTarja Systa, Albert Zundorf
Publication statusPublished - 2002

Keywords

  • Automata
  • Live Sequence Charts
  • Scenario
  • LSCs
  • Reactive System
  • Synthesis

Fingerprint

Dive into the research topics of 'Turning High-Level Live Sequence Charts into Automata'. Together they form a unique fingerprint.

Cite this