Modeling and verifying asynchronous communication mechanisms using coloured Petri nets

Asynchronous data communication mechanisms (ACMs) have been extensively studied as data connectors between independently timed concurrent processes. In previous work, two automatic ACM synthesis methods have been proposed. However, problems remain unresolved with the most asynchronous type of ACMs, the overwriting and rereading bounded buffer (OWRRBB), especially with buffer sizes greater than one. In this work, a method of systematic modeling and verification of multi-cell OWRRBBs is presented. This method supports the study of these kinds of ACMs with regard to vital data and temporal characteristics.