Steam Boiler: Extended FOCUS Specification and its Verification in Isabelle/HOL

Title:: Steam Boiler: Extended FOCUS Specification and its Verification in Isabelle/HOL
Document type:: Technical Report
Author(s):: Maria Spichkova
Abstract:: The main idea of this case study was taken from [1]. This paper represents an extension of the Focus specification [1] of the steam boiler, its translation in Isabelle/HOL [2] and the corresponding formal Isabelle/HOL proofs for the translated specifications, which show that the specified steam boiler architecture fulfills the specified steam boiler requirements.
Keywords:: FOCUS; Isabelle; HOL; specification; verification; refinement; steam boiler
Year:: 2007
Year / month:: 2007-01-01 00:00:00
Pages:: 20
BibTeX

Occurrences: