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. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Gorgônio, K., Cortadella, J., & Xia, F. (2007). A compositional method for the synthesis of asynchronous communication mechanisms. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4546 LNCS, pp. 144–163). Springer Verlag. https://doi.org/10.1007/978-3-540-73094-1_11
Mendeley helps you to discover research relevant for your work.