Requirements Analysis of Real-Time Control Systems using PVS

This paper presents a practical application of the PVS theorem prover involving requirements analysis of real-time control systems. This work was conducted within the SafeFM project and relied on a real world avionics case study. We show how PVS was used to formalize the software requirements for the system and to verify safety-related properties. We also present the main result of the experiment. We give an overview of PVS libraries which were developed after the case study experiment and are intended to facilitate the specification and verification of similar systems. 1 Introduction The SafeFM project 1 investigated the practical application of formal methods to the development and assessment of high integrity systems [17]. Within the project, we investigated the use of formal methods and theorem proving in requirement analysis of realtime control systems. A major part of this work involved an experiment applying the PVS theorem prover to the analysis of an avionics control system..