Concurrency model and its application to formal specifications of asynchronous protocols

A concurrency model of asynchronous protocols is presented. Concurrent events, concurrency blocks, global states, concurrency measures, communication deadlocks and data races are defined based on the model. The model allows high-level abstractions to be used for understanding concurrent behaviors of asynchronous protocols. Based on the concept of concurrency blocks, we show how to compute concurrency measures efficiently and compare the concurrency measures of asynchronous protocols with that of synchronous protocols. The model is applied to the formal description techniques, Estelle and SDL, to reason and classify their concurrent behaviors