Synthesizing a proper implementation for a scenario-based
specification is often impossible, due to the distributed nature of implementations.
To be able to detect problematic specifications, realizability
criteria have been identified, such as non-local choice.
In this work we develop a formal framework to study realizability
of compositional MSC [GMP03]. We use it to derive a complete classification
of criteria that is closely related to the criteria for MSC from
[MGR05]. Comparing specifications and implementations is usually complicated,
because different formalisms are used. We treat both of them
in terms of a single formalism. Therefore we extend the partial order
semantics of [Pra86, KL98] with a way to model deadlocks and with a
more sophisticated way to address communication.
|Title of host publication||Algebraic Methodology and Software Technology (Proceedings 11th International Conference, AMAST 2006, Kuressaare, Estonia, July 5-8, 2006)|
|Editors||M. Johnson, V. Vene|
|Place of Publication||Berlin|
|Publication status||Published - 2006|
|Name||Lecture Notes in Computer Science|