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 , 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 , and refine the PVS Real-Time method (PVS-RT) outlined in .
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.
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.
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.