AsmL Specification and Verification of Lamport’s Bakery Algorithm

Matko Botinčan

Abstract


We present a specification of Lamport’s Bakery algorithm written in AsmL specification language. By exploration of the state space of the induced labeled transition system we show how to verify important safety and liveness properties of the algorithm.

Full Text:

PDF


DOI: https://doi.org/10.2498/cit.2005.04.09

Creative Commons License
This work is licensed under a Creative Commons Attribution-NoDerivatives 4.0 International License.

Crossref Similarity Check logo

Crossref logologo_doaj