Turning High-Level Live Sequence Charts into Automata

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

Fingerprint

Semantics
Specifications
Chemical analysis

Keywords

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

Cite this

Bontemps, Y., & Heymans, P. (2002). Turning High-Level Live Sequence Charts into Automata. In T. Systa, & A. Zundorf (Eds.), Proceedings of the First International Workshop on Scenarios and State Machines (SCESM), (ICSE'02 workshop)
Bontemps, Yves ; Heymans, Patrick. / Turning High-Level Live Sequence Charts into Automata. Proceedings of the First International Workshop on Scenarios and State Machines (SCESM), (ICSE'02 workshop). editor / Tarja Systa ; Albert Zundorf. 2002.
@inproceedings{657638f5b7394ee3941d20e0a9f5c9d7,
title = "Turning High-Level Live Sequence Charts into Automata",
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.",
keywords = "Automata, Live Sequence Charts, Scenario, LSCs, Reactive System, Synthesis",
author = "Yves Bontemps and Patrick Heymans",
note = "Publication editors : Tarja Systa and Albert Zundorf",
year = "2002",
language = "English",
editor = "Tarja Systa and Albert Zundorf",
booktitle = "Proceedings of the First International Workshop on Scenarios and State Machines (SCESM), (ICSE'02 workshop)",

}

Bontemps, Y & Heymans, P 2002, Turning High-Level Live Sequence Charts into Automata. in T Systa & A Zundorf (eds), Proceedings of the First International Workshop on Scenarios and State Machines (SCESM), (ICSE'02 workshop).

Turning High-Level Live Sequence Charts into Automata. / Bontemps, Yves; Heymans, Patrick.

Proceedings of the First International Workshop on Scenarios and State Machines (SCESM), (ICSE'02 workshop). ed. / Tarja Systa; Albert Zundorf. 2002.

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

TY - GEN

T1 - Turning High-Level Live Sequence Charts into Automata

AU - Bontemps, Yves

AU - Heymans, Patrick

N1 - Publication editors : Tarja Systa and Albert Zundorf

PY - 2002

Y1 - 2002

N2 - 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.

AB - 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.

KW - Automata

KW - Live Sequence Charts

KW - Scenario

KW - LSCs

KW - Reactive System

KW - Synthesis

M3 - Conference contribution

BT - Proceedings of the First International Workshop on Scenarios and State Machines (SCESM), (ICSE'02 workshop)

A2 - Systa, Tarja

A2 - Zundorf, Albert

ER -

Bontemps Y, Heymans P. Turning High-Level Live Sequence Charts into Automata. In Systa T, Zundorf A, editors, Proceedings of the First International Workshop on Scenarios and State Machines (SCESM), (ICSE'02 workshop). 2002