2011/06/07 by Federico Buti, Massimo Callisto De Donato, Flavio Corradini +2
Computer Science · #cs.LO
paper · pdf · doi:10.4204/eptcs.54.4
published as EPTCS 54, 2011, pp. 45-59 · In Proceedings GandALF 2011, arXiv:1106.0814
arxiv created 2011/06/07 · arxiv updated 2011/06/08
In this paper we study the liveness of several MUTEX solutions by representing them as processes in PAFAS s, a CCS-like process algebra with a specific operator for modelling non-blocking reading behaviours. Verification is carried out using the tool FASE, exploiting a correspondence between violations of the liveness property and a special kind of cycles (called catastrophic cycles) in some transition system. We also compare our approach with others in the literature. The aim of this paper is twofold: on the one hand, we want to demonstrate the applicability of FASE to some concrete, meaningful examples; on the other hand, we want to study the impact of introducing non-blocking behaviours in modelling concurrent systems.