Asynchronous System Synthesis

We propose a method to synthesize a set of components from a high-level
specification of the intended behaviour of the target system. The designer
proceeds via correctness-preserving transformation steps towards an
implementable architecture of components which communicate
asynchronously. The interface model of each component specifies the used
communication protocol. At each step a pre-defined component is extracted
and the correctness of the step is proved. This ensures the compatibility of
the components. We use Action Systems as our formal approach to system
design. The method is inspired by hardware oriented approaches with their
component libraries, but is more general. We also explore the possibility of
using tool support to administrate the derivation, as well as to assist in
correctness proofs. Here we rely on the tools supporting the B Method, as
this method is closely related to Action Systems and has good tool support.