Automated Analysis of MUTEX Algorithms with FASE

Federico Buti
(University of Camerino)
Massimo Callisto De Donato
(University of Camerino)
Flavio Corradini
(University of Camerino)
Maria Rita Di Berardini
(University of Camerino)
Walter Vogler
(University of Augsburg)

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.

In Giovanna D'Agostino and Salvatore La Torre: Proceedings Second International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2011), Minori, Italy, 15-17th June 2011, Electronic Proceedings in Theoretical Computer Science 54, pp. 45–59.
Published: 4th June 2011.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: