Where academic tradition
meets the exciting future

Formal Stepwise Development of an In-House Temperature Control System

Mats Neovius, Formal Stepwise Development of an In-House Temperature Control System. TUCS Technical Reports 1078, TUCS, 2013.

Abstract:

With the possibility to sense and control the physical environment, restrictions and demands on how it is controlled may be defined. The system guaranteeing the stated conditions by analysing the sensory data and triggering a corrective action is called a control system. Formal verification ascertains the correct mathematical functionality of such a control system given a model of the environment. Moreover, formal specification facilitates the engineers’ understanding of the system features. In this report, we formally specify a temperature control system responsible for maintaining a certain in-house temperature in the Event-B language. We verify this specification in the Rodin Platform tool. The specification is developed independently in a stepwise manner to be suitable for integration with other control systems.

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tNeovius_Mats13a,
  title = {Formal Stepwise Development of an In-House Temperature Control System},
  author = {Neovius, Mats},
  number = {1078},
  series = {TUCS Technical Reports},
  publisher = {TUCS},
  year = {2013},
  keywords = {Formal modelling, Event-B, refinement, temperature control, control system, adaptive house},
  ISBN = {978-952-12-2893-3},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Edit publication