期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2011
卷号：54
页码：45-59
DOI：10.4204/EPTCS.54.4
出版社：Open Publishing Association
摘要：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.
