This paper presents a practical application of the PVS theorem prover involving requirements analysis of real-time control systems. This work was con ducted 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 in tended to facilitate the specification and verification of similar systems.

• lfm97.ps