DocumentCode :
3614856
Title :
Verification of Bakery algorithm variants for two processes
Author :
D. Dedic;R. Meolic
Author_Institution :
Nova Vizija d.o.o., Zalec, Slovenia
Volume :
2
fYear :
2003
fDate :
6/25/1905 12:00:00 AM
Firstpage :
35
Abstract :
This paper is about Bakery algorithm for mutual exclusion. Three variants of the algorithm for two processes are discussed, formally modelled with a simple process algebra and then verified. Two methods of verification are given. In the first one, the processes representing behaviour of the algorithms are minimised with regard to testing equivalence and then examined. In the second approach, the properties are expressed with temporal logic ACTL and then verified using a model checker. Because we bounded the possible values of variables, the paper contributes new results and knowledge to the well-known facts about Bakery algorithm.
Keywords :
"Computer science","Logic","System testing","Centralized control","Read-write memory"
Publisher :
ieee
Conference_Titel :
EUROCON 2003. Computer as a Tool. The IEEE Region 8
Print_ISBN :
0-7803-7763-X
Type :
conf
DOI :
10.1109/EURCON.2003.1248140
Filename :
1248140
Link To Document :
بازگشت