User: Guest  Login
Document type:
Technical Report 
Author(s):
Maria Spichkova 
Title:
Steam Boiler: Extended FOCUS Specification and its Verification in Isabelle/HOL 
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