This paper proposes an original framework for modelling and verification (M&V) of starvation-free mutual exclusion algorithms based on weak semaphores, that are without a built-in waiting-process queue. The goal is to support the implementation of light-weight starvation-free semaphores useful in general concurrent systems including cyber physical systems. The M&V approach depends on UPPAAL. First known weak semaphores are modelled. Then they are exploited for model checking classic algorithms. Known properties are retrieved but subtle new ones are discovered. As part of the developed approach, a new algorithm is proposed which uses two semaphores of the weakest type, N bits (N being the number of processes) and a counter. This algorithm too is proved to be correct.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo
|Titolo:||Modelling and Verification of Starvation-Free Mutual Exclusion Algorithms based on Weak Semaphores|
CICIRELLI, Franco [Membro del Collaboration Group]
NIGRO, Libero [Membro del Collaboration Group] (Corresponding)
|Data di pubblicazione:||2015|
|Appare nelle tipologie:||4.1 Contributo in Atti di convegno|