Verification of Real-Time Control Software Using PVS

by M. Lawford and H. Wu

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.

Download

ciss.ps (postscript 178k) or ciss.pdf (pdf 187k)

BibTeX Entry

@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",
}