Difference between revisions of "Development of a Heating Controller System"
imported>Reza |
imported>Reza |
||
Line 63: | Line 63: | ||
==System Decomposition== | ==System Decomposition== | ||
[[Image:Decomp1.jpg|Centre]] | [[Image:Decomp1.jpg|Centre]] | ||
+ | |||
+ | Second level decomposition | ||
+ | In this stage we decompose the controller to some tasks that communicating through a shared object. | ||
[[Image:Decomp2.jpg|Centre]] | [[Image:Decomp2.jpg|Centre]] |
Revision as of 10:38, 15 April 2011
Introduction
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
In this diagram an overview of the Heating Controller and its related components are presented. The controller in the middle of the diagram communicates inputs and outputs parameters with its surrounding components. At the top there are two buttons that allow the user to increase/decrease Target Temperature. The target temperature periodically will be sent by the controller to the related display to be shown to the outside world. The controller uses two Temperature Sensors to poll the environment temperature. The average of the values read from these two sensors is calculated and displayed by the controller on the Current Temperature Display. If the current temperature is lower than the target temperature, the controller will turn on the heater source using Heat Source Switch, otherwise this switch will be turned off by the controller. The status of the heater itself also will be monitored through the Heater Sensor. If due to some faults the heater is not working properly, the controller will activate either of Over-temperature or No-heat Alarms
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
Interfaces | Types | Definitions |
---|---|---|
Temperature Sensors | Integer | Temperature in degrees Celsius |
Heater Sensors | Boolean | True when heater is at working temperature, False otherwise |
Heat Source Switch | Boolean | True when activated, False otherwise |
No-heat Alarm | Boolean | True when activated, False otherwise |
Over-temperature Alarm | Boolean | True when activated, False otherwise |
Current temperature Display | Integer | Average temperature value in degrees Celsius |
Target temperature | Integer | Target temperature value in degrees Celsius |
An Overview of the System Development
System Decomposition
Second level decomposition
In this stage we decompose the controller to some tasks that communicating through a shared object.