Formal verification of the PATHO real-time operating system

17 December 2002

conference paper
Published by Institute of Electrical and Electronics Engineers (IEEE)

Vol. 3, 2459-2465 vol.3
https://doi.org/10.1109/cdc.1994.411507

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

This publication has 7 references indexed in Scilit:

Automata for modeling real-time systems
Published by Springer Nature ,2005
Iterative Algorithms For Formal Verification Of Embedded Real-time Systems
Published by Institute of Electrical and Electronics Engineers (IEEE) ,2005
Model-checking for real-time systems
Published by Institute of Electrical and Electronics Engineers (IEEE) ,2002
HSIS
Published by Association for Computing Machinery (ACM) ,1994
Smart cars on smart roads: problems of control
IEEE Transactions on Automatic Control, 1993
Analysis of discrete event coordination
Published by Springer Nature ,1990
Automatic verification of finite-state concurrent systems using temporal logic specifications
ACM Transactions on Programming Languages and Systems, 1986