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.

Abstract
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.
Files
 













 

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