Modelling and Verification of Mutual Exclusion Algorithms
Modelling and Verification of Mutual Exclusion Algorithms
This paper proposes modelling and exhaustive verification of mutual exclusion algorithms using timed automata (TA) and the popular UPPAAL toolbox. The proposal allows to check all the properties of a mutual clusion algorithm also along the time dimension. Both the classic case of atomic read/write operations on memory cells and the non determinism of reading a memory cell during one or multiple write operations on it as it may occur in modern multi-port memories are considered. The approach is then applied to some algorithms proposed in the literature of which known properties are confirmed but also new ones are revealed.
timed automata, atomic vs. non atomic read/write operations, Mutual exclusion algorithms, atomic vs. non atomic read/write operations,; timed automata, model checking, ; UPPAAL, Mutual exclusion algorithms, model checking, UPPAAL
timed automata, atomic vs. non atomic read/write operations, Mutual exclusion algorithms, atomic vs. non atomic read/write operations,; timed automata, model checking, ; UPPAAL, Mutual exclusion algorithms, model checking, UPPAAL
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).2 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!