Formal Verification of Real-Time Software

Mr. Hongyu Wu


The verification of functionality of the input/output logic properties often composes the majority of software requirements analysis. Automated theorem provers (ATPs) such as SRI's Prototype Verification System (PVS) have been successfully used in the formal verification of functional properties. However, such functional methods are not readily applicable to the verification of the real-time software requirements.

The thesis continues the research summarized in [2], focusing on extending functional verification methods to the verification of real-time control properties through the development of a PVS library for the specification and verification of real-time control system. More specifically, we extend the PVS ``Clocks'' and ``Held_For'' theories originally defined in [] and [2], and refine the PVS Real-Time method (PVS-RT) outlined in [2]. New developments of the thesis include the definition of strong clock induction and several lemmas regarding real-time properties. These definitions, when combined with PVS's support for the tabular methods provide a useful environment for the specification and verification of basic real-time control properties.

To illustrate the utility of the PVS-RT method, we perform the verification of two timing blocks of an industrial real-time control system. The PVS specification and proof techniques are described in sufficient details to show how errors or invalid assumptions are detected in the proposed implementation and the original specifications. Finally we prove that corrected versions of the implementation satisfy the updated versions of the specifications.

[1]B. Dutertre and V.Stavridou, ``Formal requirements analysis of an avionics control system,'' IEEE Transactions on Software Engineering, vol.23, pp.267--278, May 1997.

[2]M. Lawford and H. Wu, ``Verification of real-time control software using PVS''. In: P. Ramadge and S. Verdu (eds.): Proceedings of the 2000 Conference on Information Sciences and Systems, Vol.2. Princeton, NJ, pp. TP1--13--TP1--17, 2000.