Development of a Heating Controller System: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Reza
imported>Reza
Line 10: Line 10:
* Displaying Current Temperature
* Displaying Current Temperature
* Power on/off Heater  
* Power on/off Heater  
* Sensing heater status
* Sensing the heater status
* Activating/Deactivating No Heat Alarms
* Activating/Deactivating No Heat Alarm
* Activating/Deactivating Over-Heat Alarm
* 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 the heater status
  • Activating/Deactivating No Heat Alarm
  • Activating/Deactivating Over-Heat Alarm