Arjan Mooij (OAS Group)

Title: Realizability criteria for compositional MSC


Abstract:

Synthesizing proper implementations for
scenario-based specifications is often impossible,
due to the discrepancy between the global nature of specifications and
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
in which various realizability criteria are studied,
and completeness of our earlier classification is shown.
Not only specifications but also implementations
are treated in terms of partial orders,
because such a formalism is close to the nature of MSC specifications,
and it avoids dealing with the typical over-specific linearizations.
We extend the partial order semantics of [Katoen-Lambert]
such that compositional MSC and deadlocks can be addressed.