When synchronous programming is used for the design of communication protocols or other similar processes embedded in a larger asynchronous setting, the environment becomes the network medium, through which messages are exchanged on their way between several (synchronous) nodes. Properties of correction often must deal with the full system as a whole, and thus the network must be explicitly modeled and connected with the individual synchronous nodes in formal way.

At some abstract level we shall usually model the network as some collection of bounded FIFO buffers --or variants of such with possible message loss or duplication. While each medium can be itself modeled as a synchronous (or asynchronous) process, the communication between synchronous protocol nodes and the network must consist of synchronizing rendez-vous (or else messages could be unduly ignored).

The finite state aspect of media buffers is important to us since we want to apply symbolic model-checking techniques based on BDDs, so that the full state space must be modeled on a finite bit vector. The main issue concerning algorithmic efficiency is to combine the partitioning methods that allow not to represent the full transition relations, either in the synchronous or in the asynchronous sub-cases. To be specific, the transition relation is split along each boolean state element (or, latch register) in the synchronous framework, while it is split along each  synchronous site in the  larger asynchronous network. Keeping both partitioning techniques in a framework where asynchronous networks of synchronous processes are concerned is a key to the successful reachable state space computation of large systems.

In this deliverable we provide means to synthesize networks in a formal ways from succinct user descriptions of buffers (size, features and  finite type message values). We also provide ways to specify distant message send/receive actions in a synchronous node. We face the algorithmic issues underlying the methods mentioned above. In the coming years we intend to implement this (reusing parts of existing verification softwares in the pure asynchronous or synchronous cases), and conduct case studies.