Technical Report
The Steamboiler Specification - A Case Study in Focus
Author(s): Manfred Broy, Franz Regensburger, Bernhard Schätz, Katharina Spies
Year: 1997
Number: TUM-I9714
Editor:
CR Classification: D.2.1, D.2.4, D.2.10, F.3.1, F.3.2
CR General Terms: Design, Security, Theroy, Verification
Keywords: Case Study, Focus, Formal, Method, Safety-Critical, Refinement, Fault-Tolerant, Control Theory, Model, State, Description, Table
Abstract:This paper sketches the expressiveness and the usefulness of the well-tuned
concepts of FOCUS by its application of the requirements specification of a
steam boiler, see [Abr96]. We demonstrate the support for non-specialists in
formal methods by using user-friendly description techniques, here the
state-oriented specification with table notation techniques, and a broad range
of refinement techniques, here the concept of data and state refinement, which
eases the explicit modeling of fault-tolerant behavior. Additionally we prove
its adaptability in different domains by handling an example of the "control
theory” application field. Because of complexity of the above mentioned aspects
we do not give a complete and detailed specification, but rather concentrate on
the control task starting from classical control theory, the conceptual formal
model of FOCUS and its possibilities for formal modeling and system development.
Available as compressed Postscript
BibTeX-Entry:
<![CDATA[
@techreport{BRSS97,
author = {Manfred Broy and Franz Regensburger and Bernhard Schätz and Katharina Spies},
title = {The Steamboiler Specification - A Case Study in Focus},
number = {TUM-I9714},
institution = {Technische Univerit\"at M\"unchen},
year = {1997},
url = {http://www4.informatik.tu-muenchen.de/reports/BRSS97.html},
abstract = {This paper sketches the expressiveness and the usefulness of the well-tuned
concepts of FOCUS by its application of the requirements specification of a
steam boiler, see [Abr96]. We demonstrate the support for non-specialists in
formal methods by using user-friendly description techniques, here the
state-oriented specification with table notation techniques, and a broad range
of refinement techniques, here the concept of data and state refinement, which
eases the explicit modeling of fault-tolerant behavior. Additionally we prove
its adaptability in different domains by handling an example of the "control
theory” application field. Because of complexity of the above mentioned aspects
we do not give a complete and detailed specification, but rather concentrate on
the control task starting from classical control theory, the conceptual formal
model of FOCUS and its possibilities for formal modeling and system development.},
CRClassification = {D.2.1, D.2.4, D.2.10, F.3.1, F.3.2},
CRGenTerms = {Design, Security, Theroy, Verification}}
]]>