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
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;
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
DOI :
10.1109/SLFSTB.1999.777484
