Turning High-Level Live Sequence Charts into Automata

Yves Bontemps; Patrick Heymans

Turning High-Level Live Sequence Charts into Automata

Faculte d'informatique

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférence › Article dans les actes d'une conférence/un colloque

Résumé

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.

langue originale	Anglais
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

Accès au document

http://www.info.fundp.ac.be/~ybo/docs/icse02/icse02.pdf

Contient cette citation

@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)",

}

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.

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférence › Article dans les actes d'une conférence/un colloque

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 -

Turning High-Level Live Sequence Charts into Automata

Résumé

Accès au document

Empreinte digitale

Contient cette citation