DocumentCode
2955082
Title
A case-study in component-based mechanical verification of fault-tolerant programs
Author
Kulkarni, Sandeep S. ; Rushby, John ; Shankar, Nishanth
Author_Institution
Dept. of Comput. & Inf. Sci., Ohio State Univ., Columbus, OH, USA
fYear
1999
fDate
1999
Firstpage
33
Lastpage
40
Abstract
We present a case study to demonstrate that the decomposition of a fault tolerant program into its components is useful in its mechanical verification. More specifically we discuss our experience in using the theorem prover PVS to verify Dijkstra´s token ring program in a component based manner. We also demonstrate the advantages of component based mechanical verification
Keywords
program verification; software fault tolerance; theorem proving; Dijkstra token ring program; PVS; component based mechanical verification; fault tolerant programs; mechanical verification; theorem prover; Computer science; Contracts; Detectors; Fault detection; Fault tolerance; Government; Information science; Laboratories; Safety; Token networks;
fLanguage
English
Publisher
ieee
Conference_Titel
Self-Stabilizing Systems, 1999. Proceedings. 19th IEEE International Conference on Distributed Computing Systems Workshop on
Conference_Location
Austin, TX
Print_ISBN
0-7695-0228-8
Type
conf
DOI
10.1109/SLFSTB.1999.777484
Filename
777484
Link To Document