DocumentCode
2567708
Title
Verification of fault tolerance and real time
Author
Liu, Zhiming ; Joseph, Mathai
Author_Institution
Dept. of Math. & Comput. Sci., Leicester Univ., UK
fYear
1996
fDate
25-27 Jun 1996
Firstpage
220
Lastpage
229
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Fault Tolerant Computing, 1996., Proceedings of Annual Symposium on
Conference_Location
Sendai
ISSN
0731-3071
Print_ISBN
0-8186-7262-5
Type
conf
DOI
10.1109/FTCS.1996.534609
Filename
534609
Link To Document