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.


Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST, Axel Rennoch