Abstract: This paper provides preliminary results from an investigation of the use of PVS for the specification and verification of the real-time behavior of control systems software. Preliminary definitions are developed for specifying real-time software requirements. The definitions are used to specify a subsystem of an industrial real-time control system and then PVS is used to detect several errors in a proposed implementation and the original specification. Finally we prove that a corrected version of the implementation satisfies the updated version of the specification.
ciss.ps (postscript 178k) or ciss.pdf (pdf 187k)
@InProceedings{LawWu00, author = {M. Lawford and H. Wu}, title = {Verification of real-time control software using PVS}, booktitle = {Proceedings of the 2000 Conference on Information Sciences and Systems}, year = "2000", editor = {P. Ramadge and S. Verdu}, pages = "TP1-13--TP1-17", volume = "2", publisher = "Dept.\ of Electrical Engineering, Princeton University", address = "Princeton, NJ", month = mar, key = "LawWu00", }