Development of a Heating Controller System: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Reza
No edit summary
imported>Reza
Line 5: Line 5:


==Main functionaly of the system==
==Main functionaly of the system==
Adjusting Target Temperature
* Provideing interface to adjust Target Temperature
Sensing temperature
* Displaying new Target Temperature
Displaying current and target temperatures
* Sensing Current Temperature
Activating/Deactivating Alarms
* Displaying Current Temperature
Change target temperature
* Power on/off Heater  
Power on/off Heater  
* Sensing heater status
Sensing heater status
* Activating/Deactivating No Heat Alarms
* Activating/Deactivating Over-Heat Alarm

Revision as of 18:41, 13 April 2011

This section describes an Event-B development of a simple heating controller. This is a first case study that covers the entire development process; starting from a system specification and ending up in an implementation in the Ada programing language. The development process starts with an abstract specification followed by two successive refinements before decomposing the model to two separate sub-models. The refinement process continues after the first decomposition in order to arrive at a concrete level suitable for implementation. This allows us to devise an appropriate tasking structure that needed by the code generation plug-in. The outcomes of the second decomposition are a number of tasking machines plus a specific type of machine for representing protected shared data. This protected shared data facilitating communications between taking machines. Then we illustrate how using the code generation plug-in a concurrent Ada implementation is generated. The overall aim of this case study is to put in practice the recommended methodological aspects of Event-B, particularly those aspects of modelling concerned with decomposition and code generation.

System Architecture

Main functionaly of the system

  • Provideing interface to adjust Target Temperature
  • Displaying new Target Temperature
  • Sensing Current Temperature
  • Displaying Current Temperature
  • Power on/off Heater
  • Sensing heater status
  • Activating/Deactivating No Heat Alarms
  • Activating/Deactivating Over-Heat Alarm