Asynchronous data communication mechanisms (ACMs) have been extensively studied as data connectors between independently timed
concurrent processes. In previous work, an automatic ACM synthesis method based on the generation of the reachability graph
and the theory of regions was proposed. In this paper, we propose a new synthesis method based on the composition of Petri
net modules, avoiding the exploration of the reachability graph. The behavior of ACMs is formally defined and correctness
properties are specified in CTL. Model checking is used to verify the correctness of the Petri net models. The algorithms
to generate the Petri net models are presented. Finally, a method to automatically generate C++ source code from the Petri
net model is described.
Keywords Asynchronous communication mechanisms - Petri nets - concurrent systems - synthesis - model checking - protocols