文章基本信息

标题：Automated Analysis of MUTEX Algorithms with FASE
本地全文：下载
作者：Federico Buti ; Massimo Callisto De Donato ; Flavio Corradini 等
期刊名称：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.