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

Specification and Verification od the Real-Time Part of a Steam Boiler Control System
 by Jan Vitt & Jozef Hooman.

The goal of this paper is the correct derivation of an implementation of a steam boiler control system. Using a mixed formalism that is presented in [Hoo94b] in which programs and assertional specifications are combined within a unified framework, we refine its top-level specification in a top-down manner. Having the formalism defined in the PVS specification language, the interactive proof checker of PVS is used to check the correctness of each refinement step, therby guarateeing the correctness of the resulting program.


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