5th International Workshop on
Formal Methods for Industrial Critical Systems
Berlin, April 3-4, 2000
Conditions for synthesis of communicating
automata from HMSCs
Formal methods can now be used at early stages of the development process. This
increases the need for consistency between two levels of formalisms: a declarative
level of scenario type, and an operational level of automata type. It is particularly
true in the telecommunications world with the joint use of standardized languages
like High-level Message Sequence Charts (HMSCs) and SDL. So it is natural to
consider the transition from one level to another by automated synthesis mechanisms. Algorithms for synthesis of SDL communicating systems from HMSCs have
been proposed these last years. However, the theoretical power of HMSCs is such
that only a subset of HMSCs can be reasonably treated. Identification of the limits
of synthesis is still in its early stages. In this article we show for the first time a
necessary condition so that synthesis preserves behaviours. This condition relies on
a property of generalized local choice and reconstructibility of the local sequencing.
It is decidable and we present algorithms that could be implemented in practical
synthesis tools.
Note: The content of the following files is part of
GMD Report No. 91
and subject to its copyright.
ERCIM FMICS Home Page,
GMD FOKUS Home Page
Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST,
Axel Rennoch