Development of a Heating Controller System - Revision history

imported>Reza: /* System Architecture */

2011-05-12T10:06:28Z

System Architecture

← Older revision		Revision as of 10:06, 12 May 2011
Line 59:		Line 59:
	\|True when activated, False otherwise		\|True when activated, False otherwise
	\|-		\|-
	\|Current temperature ~~Display~~		\|Current temperature
	\|Integer		\|Integer
	\|Average temperature value in degrees Celsius		\|Average temperature value in degrees Celsius

imported>Reza: /* System Architecture */

2011-05-12T10:04:00Z

System Architecture

← Older revision		Revision as of 10:04, 12 May 2011
Line 43:		Line 43:
	\|Temperature in degrees Celsius		\|Temperature in degrees Celsius
	\|-		\|-
	\|Heater ~~Sensors~~		\|Heater Sensor
	\|Boolean		\|Boolean
	\|True when heater is at working temperature, False otherwise		\|True when heater is at working temperature, False otherwise

imported>Reza: /* The Tasking Event-B Tutorial */

2011-05-06T17:30:31Z

The Tasking Event-B Tutorial

← Older revision		Revision as of 17:30, 6 May 2011
Line 95:		Line 95:
	Now that we have fully developed Event-B models that encompass basic structures for tasks we can move to the next stage. This is to generate an executable Ada code for the system using the code generation plug-in. This is the first time that this plug-in explored extensively; therefore we present the next stage in the form of a tutorial.		Now that we have fully developed Event-B models that encompass basic structures for tasks we can move to the next stage. This is to generate an executable Ada code for the system using the code generation plug-in. This is the first time that this plug-in explored extensively; therefore we present the next stage in the form of a tutorial.

	The Tasking Event-B tutorial starts [[Tasking Event-B Tutorial\|here]].		The Tasking Event-B tutorial starts [[Tasking Event-B Tutorial\|here]]. Also a link to an archive file, which includes the complete development, can be found on this page.

imported>Reza: /* The Tasking Event-B Tutorial */

2011-05-06T17:25:18Z

The Tasking Event-B Tutorial

← Older revision		Revision as of 17:25, 6 May 2011
Line 93:		Line 93:

	=== The Tasking Event-B Tutorial ===		=== The Tasking Event-B Tutorial ===
			Now that we have fully developed Event-B models that encompass basic structures for tasks we can move to the next stage. This is to generate an executable Ada code for the system using the code generation plug-in. This is the first time that this plug-in explored extensively; therefore we present the next stage in the form of a tutorial.

	The Tasking Event-B tutorial starts [[Tasking Event-B Tutorial\|here]].		The Tasking Event-B tutorial starts [[Tasking Event-B Tutorial\|here]].

imported>Reza: /* Second level decomposition */

2011-05-06T17:08:31Z

Second level decomposition

← Older revision		Revision as of 17:08, 6 May 2011
Line 89:		Line 89:

	===Second level decomposition===		===Second level decomposition===
	In this stage we decompose the controller to ~~some~~ tasks ~~that communicating~~ through a shared object. Note that tasks still are able to communicate with the environment directly.		In this stage we decompose the controller to three different tasks which interacting with each other through a shared object. This structure is presented in the following figure. Note that tasks still are able to communicate with the environment directly. In practice the number of the tasks and the way that we distribute different events over these tasks are determined by various factors. Other properties of tasks, such as their priorities, whether they are periodic or not, and the length of each periodic task in millisecond are defined later in the tasking development stage.
	[[Image:Decomp2.jpg\|center]]		[[Image:Decomp2.jpg\|center]]

imported>Mathieu: /* The Tasking Event-B Tutorial */

2011-05-05T09:00:53Z

The Tasking Event-B Tutorial

← Older revision		Revision as of 09:00, 5 May 2011
Line 94:		Line 94:
	=== The Tasking Event-B Tutorial ===		=== The Tasking Event-B Tutorial ===

	The Tasking Event-B tutorial starts [~~http://wiki.event-b.org/index.php?title=Tasking_Event~~-~~B_Tutorial~~ here]		The Tasking Event-B tutorial starts [[Tasking Event-B Tutorial\|here]].

imported>Reza: /* Introduction */

2011-05-04T11:05:38Z

Introduction

← Older revision		Revision as of 11:05, 4 May 2011
Line 1:		Line 1:
	{{TOCright}}		{{TOCright}}
	==Introduction==		==Introduction==
	This section describes an Event-B development of a simple heating controller. This is the first case study to cover the entire development process; starting from a system specification and ending up with implementable Ada code. The development process starts with an abstract specification followed by two successive refinements, we then decompose the model into two separate sub-models representing the environment and the rest of the system. The refinement process continues after the first decomposition in order to arrive at a concrete level suitable for implementation. This allows us to derive the appropriate tasking structure that is needed by the code generation plug-in. The second decomposition gives rise to a number of tasking machines, plus a specific type of machine for representing protected shared data. This protected shared data facilitating communications between tasking 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.		This section describes an Event-B development of a simple heating controller. This is the first case study to cover the entire development process; starting from a system specification and ending up with implementable Ada code. The development process starts with an abstract specification followed by two successive refinements, we then decompose the model into two separate sub-models representing the environment and the rest of the system. The refinement process continues after the first decomposition in order to arrive at a concrete level suitable for implementation. This allows us to derive the appropriate tasking structure that is needed by the code generation plug-in. The second decomposition gives rise to a number of tasking machines, plus a specific type of machine for representing protected shared data. This protected shared data facilitating communications between tasking 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==		==System Architecture==

imported>Andy: /* An Overview of the System Development */

2011-05-04T10:43:40Z

An Overview of the System Development

← Older revision		Revision as of 10:43, 4 May 2011
Line 69:		Line 69:

	==An Overview of the System Development==		==An Overview of the System Development==
	Before discussing Event-B models the Heater Controller in more detail, it is useful to provide an overview of the development approach. In this section we demonstrate this with a diagram. Starting from the top level of the diagram, it shows the most abstract model of the system or as it know as the system specification. In this stage we have specified the main system’s functionality. This includes events for modelling increase/decrease target temperature, polling the environment temperature using two available sensors, calculating current temperature, turning on/off the heat source, and finally activating or deactivating two different alarms should it deemed to be necessary by the controller. Events in this stage are deliberately simple to achieve maximum comprehensibility. Events ordering and ~~sequencing~~ is introduced in the later stages.		Before discussing Event-B models the Heater Controller in more detail, it is useful to provide an overview of the development approach. In this section we demonstrate this with a diagram. Starting from the top level of the diagram, it shows the most abstract model of the system or as it know as the system specification. In this stage we have specified the main system’s functionality. This includes events for modelling increase/decrease target temperature, polling the environment temperature using two available sensors, calculating current temperature, turning on/off the heat source, and finally activating or deactivating two different alarms should it deemed to be necessary by the controller. Events in this stage are deliberately simple to achieve maximum comprehensibility. Events ordering and iteration is introduced in the later stages.

imported>Andy: /* An Overview of the System Development */

2011-05-04T10:40:22Z

An Overview of the System Development

← Older revision		Revision as of 10:40, 4 May 2011
Line 74:		Line 74:
	[[Image:development.jpg\|center]]		[[Image:development.jpg\|center]]

	In the first refinement level we introduce sensing and actuation which are considered as design steps. Here sensing involves polling the state of increase/decrease buttons, temperature sensors, and the heater sensor. Actuation concerns the update of target and current temperature displays with latest values, as well as sending outcomes of controller decisions to appropriate actuators such as heat on/off, and ~~different~~ alarms.		In the first refinement level we introduce sensing and actuation which are considered as design steps. Here sensing involves polling the state of increase/decrease buttons, temperature sensors, and the heater sensor. Actuation concerns the update of target and current temperature displays with latest values, as well as sending outcomes of controller decisions to appropriate actuators such as heat on/off, and various alarms.

	==System Decomposition==		==System Decomposition==

imported>Andy: /* An Overview of the System Development */

2011-05-04T10:40:08Z

An Overview of the System Development

← Older revision		Revision as of 10:40, 4 May 2011
Line 69:		Line 69:

	==An Overview of the System Development==		==An Overview of the System Development==
	Before discussing Event-B models the Heater Controller in more detail, it is useful to provide an overview of the development approach. In this section we demonstrate this with a diagram. Starting from the top level of the diagram, it shows the most abstract model of the system or as it know as the system specification. In this stage we have specified the main system’s functionality. This includes events for modelling increase/decrease target temperature, polling environment temperature using two available sensors, calculating current temperature, turning on/off the heat source, and finally activating or deactivating two ~~deferent~~ alarms should it deemed to be necessary by the controller. Events in this stage are deliberately simple to achieve maximum comprehensibility. Events ordering and sequencing is introduced in the later stages.		Before discussing Event-B models the Heater Controller in more detail, it is useful to provide an overview of the development approach. In this section we demonstrate this with a diagram. Starting from the top level of the diagram, it shows the most abstract model of the system or as it know as the system specification. In this stage we have specified the main system’s functionality. This includes events for modelling increase/decrease target temperature, polling the environment temperature using two available sensors, calculating current temperature, turning on/off the heat source, and finally activating or deactivating two different alarms should it deemed to be necessary by the controller. Events in this stage are deliberately simple to achieve maximum comprehensibility. Events ordering and sequencing is introduced in the later stages.


	[[Image:development.jpg\|center]]		[[Image:development.jpg\|center]]

	In the first refinement level we introduce sensing and actuation which are considered as design steps. Here sensing involves polling the state of increase/decrease buttons, ~~environment~~ sensors and the heater sensor. Actuation concerns ~~with updating~~ target and current temperature displays with latest values, as well as sending outcomes of controller decisions to appropriate actuators such as ~~hear~~ on/off and different alarms.		In the first refinement level we introduce sensing and actuation which are considered as design steps. Here sensing involves polling the state of increase/decrease buttons, temperature sensors, and the heater sensor. Actuation concerns the update of target and current temperature displays with latest values, as well as sending outcomes of controller decisions to appropriate actuators such as heat on/off, and different alarms.

	==System Decomposition==		==System Decomposition==