# 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 language English Proceedings of the First International Workshop on Scenarios and State Machines (SCESM), (ICSE'02 workshop) Tarja Systa, Albert Zundorf Published - 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).
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