Title :
Formal verification of the PATHO real-time operating system
Author :
Balarin, Felice ; Petty, Karl ; Sengiovanni-Vincentello, A.L. ; Varaiya, Pravin
Author_Institution :
Dept. of Electr. Eng. & Comput. Sci., California Univ., Berkeley, CA, USA
Abstract :
We present several models of PATHO, a real-time operating system for an automatically controlled vehicle. The models are simple and scalable, thus they can be used to evaluate real-time verification tools. We describe the verification of PATHO using real-time extensions of HSIS verification system. Experiments show that user-supplied guidelines are crucial for successful verification
Keywords :
operating systems (computers); program verification; real-time systems; software performance evaluation; vehicles; HSIS; PATHO; automatically controlled vehicle; formal verification; real-time operating system; real-time verification tools; user-supplied guidelines; verification system; Automata; Automatic control; Control systems; Embedded system; Formal verification; Guidelines; Operating systems; Real time systems; Safety; Vehicles;
Conference_Titel :
Decision and Control, 1994., Proceedings of the 33rd IEEE Conference on
Conference_Location :
Lake Buena Vista, FL
Print_ISBN :
0-7803-1968-0
DOI :
10.1109/CDC.1994.411507
