Formal verification of the PATHO real-time operating system
Felice Balarin, Karl F. Petty, A.L. Sengiovanni-Vincentello, Pravin P. Varaiya · 2002
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.>