Title :
Verification of fault tolerance and real time
Author :
Liu, Zhiming ; Joseph, Mathai
Author_Institution :
Dept. of Math. & Comput. Sci., Leicester Univ., UK
Abstract :
A transformational method is given for specifying and verifying fault-tolerant, real-time programs. Such a program needs to be provably correct according to both its functional and real-time requirements, despite the possible occurrence of system failures. The paper demonstrates that a suitably expressive logic for real-time systems makes it possible to naturally model the state changes caused by system failures and determine their effect on the functional and real-time properties of executions
Keywords :
algebraic specification; formal specification; program verification; real-time systems; software fault tolerance; expressive logic; fault tolerance verification; fault-tolerant system verification; functional requirements; real time systems; specification; state change; system failure; system failures; transformational method; Checkpointing; Computer science; Fault tolerance; Fault tolerant systems; Logic; Real time systems; Redundancy; Systems engineering and theory; Time factors; Timing;
Conference_Titel :
Fault Tolerant Computing, 1996., Proceedings of Annual Symposium on
Conference_Location :
Sendai
Print_ISBN :
0-8186-7262-5
DOI :
10.1109/FTCS.1996.534609
