Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications

Synthesis is the process of automatically generating a correct running system from its specification. In this paper, we suggest a translation of a Live Sequence Chart specification into a two-player game for the purpose of synthesis. We use this representation for synthesizing a reactive system, and introduce a novel algorithm for composing two such systems for two subsets of a specification. Even though this algorithm may fail to compose the systems, or to prove the joint specification to be inconsistent, we present some promising results for which the composition algorithm does succeed and saves significant running time. We also discuss options for extending the algorithm into a sound and complete one.

TACAS09.pdf
PDF file

In  Tools and Algorithms for the Construction and Analysis of Systems (TACAS'09)

Publisher  Springer Verlag
All copyrights reserved by Springer 2009.

Details

TypeInproceedings
URLhttp://dx.doi.org/10.1007/978-3-642-00768-2_9
Pages77-91
Volume5505
SeriesLNCS
> Publications > Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications