SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Requirements Analysis of Real-Time Control Systems using PVS
 by Dr. Bruno Dutertre & Victoria Stavridou.

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.


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2023 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy