D32 Modes and Fault Tolerance - Revision history

imported>Tommy at 17:37, 3 December 2010

2010-12-03T17:37:25Z

← Older revision		Revision as of 17:37, 3 December 2010
Line 45:		Line 45:
	* Integration with ProR requirements tracing framework		* Integration with ProR requirements tracing framework
	* Event-B model generation and editing driven by FT patterns		* Event-B model generation and editing driven by FT patterns

	~~[[Category:D32 Deliverable]]~~

imported>Ilya.lopatkin: /* Planning */

2010-11-25T12:55:57Z

Planning

← Older revision		Revision as of 12:55, 25 November 2010
Line 41:		Line 41:
	= Planning =		= Planning =
	Current status is version 1.0.0 for Rodin 2.0		Current status is version 1.0.0 for Rodin 2.0
			In a long term we plan:
			* A few possible usability improvements
			* Integration with ProR requirements tracing framework
			* Event-B model generation and editing driven by FT patterns

	[[Category:D32 Deliverable]]		[[Category:D32 Deliverable]]

imported>Ilya.lopatkin: /* Motivations */

2010-11-25T12:50:39Z

Motivations

← Older revision		Revision as of 12:50, 25 November 2010
Line 16:		Line 16:
	* Requirements evolve, including FT.		* Requirements evolve, including FT.

	~~The~~ state of the art ~~for~~ Event-B development ~~concerning modes and fault tolerance was that there were neither mode nor fault tolerance viewpoints defined~~. The UML-B approach of statecharts is closely related to modal views. However, the statecharts drive the development by generating Event-B models as opposed to the mode views which facilitate the development by leaving the Event-B modelling activity with the user. On the fault tolerance side, we are aware of the work on ProR framework for tracing requirements, and we plan to integrate the tracing framework with our modelling approach.		There were neither mode nor fault tolerance viewpoints in the state of the art Event-B development. The UML-B approach of statecharts is closely related to modal views. However, the statecharts drive the development by generating Event-B models as opposed to the mode views which facilitate the development by leaving the Event-B modelling activity with the user. On the fault tolerance side, we are aware of the work on ProR framework for tracing requirements, and we plan to integrate the tracing framework with our modelling approach.

	The Mode/FT Views approach is to assist the main Event-B development by an additional set of abstractions and a toolset to facilitate modal and fault tolerance development. We were motivated by the following stimuli:		The Mode/FT Views approach is to assist the main Event-B development by an additional set of abstractions and a toolset to facilitate modal and fault tolerance development. We were motivated by the following stimuli:

imported>Ilya.lopatkin: /* Overview */

2010-11-25T12:40:29Z

Overview

← Older revision		Revision as of 12:40, 25 November 2010
Line 2:		Line 2:
	The Mode and Fault Tolerance Views plug-in is a modelling environment for constructing modal and fault tolerance features in a concise manner and formally linking them to Event-B models. Fault tolerance part adds additional structural checks and reserves a place to trace FT requirements.		The Mode and Fault Tolerance Views plug-in is a modelling environment for constructing modal and fault tolerance features in a concise manner and formally linking them to Event-B models. Fault tolerance part adds additional structural checks and reserves a place to trace FT requirements.

	A Mode/FT view is a graph diagram containing modes and transitions. A mode is a general characterisation of a system behaviour. It specifies ~~the~~ operating conditions under which the system provides ~~specific functionality, and the~~ functionality. A system switches between modes through mode transitions. A mode diagram is associated with an Event-B model by mapping modes and transitions into sets of events. A correct mode diagram must exhibit an internal consistency, while the associated Event-B model is enforced to implement the mode diagram by a number of proof obligations.		A Mode/FT view is a graph diagram containing modes and transitions. A mode is a general characterisation of a system behaviour. It specifies a level of functionality and operating conditions under which the system provides this functionality. A system switches between modes through mode transitions. A mode diagram is associated with an Event-B model by mapping modes and transitions into sets of events. A correct mode diagram must exhibit an internal consistency, while the associated Event-B model is enforced to implement the mode diagram by a number of proof obligations.

	A user builds and checks a Mode/FT view in the diagram editor, makes a link to an Event-B model, and proves that the model indeed implements the view. Consequent Mode/FT views construct a refinement chain alongside Event-B development. Such chain assists the main development with an orthogonal set of documents and additional proof obligations.		A user builds and checks a Mode/FT view in the diagram editor, makes a link to an Event-B model, and proves that the model indeed implements the view. Consequent Mode/FT views construct a refinement chain alongside Event-B development. Such chain assists the main development with an orthogonal set of documents and additional proof obligations.

imported>Ilya.lopatkin: /* Planning */

2010-11-25T12:36:42Z

Planning

← Older revision		Revision as of 12:36, 25 November 2010
Line 40:		Line 40:

	= Planning =		= Planning =
			Current status is version 1.0.0 for Rodin 2.0

	[[Category:D32 Deliverable]]		[[Category:D32 Deliverable]]

imported>Ilya.lopatkin: /* Available Documentation */

2010-11-25T12:34:00Z

Available Documentation

← Older revision		Revision as of 12:34, 25 November 2010
Line 34:		Line 34:
	= Available Documentation =		= Available Documentation =
	There is a wiki page with details of the plug-in functionality, installation guide, and a simple example.		There is a wiki page with details of the plug-in functionality, installation guide, and a simple example.

	[http://wiki.event-b.org/index.php/Mode/FT_Views Plug-in wiki]		[http://wiki.event-b.org/index.php/Mode/FT_Views Plug-in wiki]

	Also, we are working on a medium-scale case study and constantly improving the usability of the tool.		Also, we are working on a medium-scale case study and constantly improving the usability of the tool.

imported>Ilya.lopatkin: /* Available Documentation */

2010-11-25T12:33:43Z

Available Documentation

← Older revision		Revision as of 12:33, 25 November 2010
Line 33:		Line 33:

	= Available Documentation =		= Available Documentation =
			There is a wiki page with details of the plug-in functionality, installation guide, and a simple example.
			[http://wiki.event-b.org/index.php/Mode/FT_Views Plug-in wiki]
			Also, we are working on a medium-scale case study and constantly improving the usability of the tool.

	= Planning =		= Planning =

	[[Category:D32 Deliverable]]		[[Category:D32 Deliverable]]

imported>Ilya.lopatkin: /* Choices / Decisions */

2010-11-25T12:27:36Z

Choices / Decisions

← Older revision		Revision as of 12:27, 25 November 2010
Line 26:		Line 26:

	= Choices / Decisions =		= Choices / Decisions =
			The main objective in the tool design was to make a simple to use environment that can be used by a non-Event-B user (e.g. requirements engineer, fault tolerance specialist), yet provides the necessary functionality for an Event-B modeller. The tool was designed to be as much an external environment to Event-B models as possible.
			* We decided not to extend the Rodin database with modal and fault tolerance elements and to keep them as separate models. This led to less platform dependencies and easier maintenance.
			* The static check is also separated from the Rodin SC, and realized by the GMF validation since it does not logically belong to Rodin / Event-B. However, since the proofs are a part of the modelling process, we properly extended the Rodin proof obligation generator.
			* A modal/FT document specifies which abstract document from the project it refines. This way our modal refinement mimics the Event-B refinement chain and allows our tool to be used with the existing types of decomposition / modularisation.
			* During the initial experiments we have identified a possible need for multiple views on a single model. We decided to keep the reference to the machine in the views which allowed to create any number of views on the same model without any changes in the machine.

	= Available Documentation =		= Available Documentation =
	= Planning =		= Planning =

	[[Category:D32 Deliverable]]		[[Category:D32 Deliverable]]

imported>Ilya.lopatkin: New page: = Overview = The Mode and Fault Tolerance Views plug-in is a modelling environment for constructing modal and fault tolerance features in a concise manner and formally linking them to Even...

2010-11-24T14:05:49Z

New page: = Overview = The Mode and Fault Tolerance Views plug-in is a modelling environment for constructing modal and fault tolerance features in a concise manner and formally linking them to Even...

New page

= Overview =
The Mode and Fault Tolerance Views plug-in is a modelling environment for constructing modal and fault tolerance features in a concise manner and formally linking them to Event-B models. Fault tolerance part adds additional structural checks and reserves a place to trace FT requirements.

A Mode/FT view is a graph diagram containing modes and transitions. A mode is a general characterisation of a system behaviour. It specifies the operating conditions under which the system provides specific functionality, and the functionality. A system switches between modes through mode transitions. A mode diagram is associated with an Event-B model by mapping modes and transitions into sets of events. A correct mode diagram must exhibit an internal consistency, while the associated Event-B model is enforced to implement the mode diagram by a number of proof obligations.

A user builds and checks a Mode/FT view in the diagram editor, makes a link to an Event-B model, and proves that the model indeed implements the view. Consequent Mode/FT views construct a refinement chain alongside Event-B development. Such chain assists the main development with an orthogonal set of documents and additional proof obligations.

The plug-in was developed in Newcastle University.

= Motivations =

We have conducted a study of approaches to complex critical systems development, and the requirements documents within DEPLOY, and arrived at the following:
* Separation of concerns is a major approach to tackle the complexity of the systems development.
* A large amount of critical systems are developed using a notion of operation modes.
* All critical systems involve operations with important aspects of human activity (e.g. lives, finance) hence critical. And all of them inevitably have faults due to changing environmental conditions, hardware failures etc. A high percentage of requirements to such systems (up to 40% according to our study within DEPLOY) include fault tolerance as a way to mitigate the consequences of errors.
* Requirements evolve, including FT.

The state of the art for Event-B development concerning modes and fault tolerance was that there were neither mode nor fault tolerance viewpoints defined. The UML-B approach of statecharts is closely related to modal views. However, the statecharts drive the development by generating Event-B models as opposed to the mode views which facilitate the development by leaving the Event-B modelling activity with the user. On the fault tolerance side, we are aware of the work on ProR framework for tracing requirements, and we plan to integrate the tracing framework with our modelling approach.

The Mode/FT Views approach is to assist the main Event-B development by an additional set of abstractions and a toolset to facilitate modal and fault tolerance development. We were motivated by the following stimuli:
* Facilitate the modal and fault tolerance development in Event-B with a comprehensible modelling approach.
* Stimulate the consideration of fault tolerance at the very first phases of development.
* Explicitly covering mode and fault tolerance concerns, we wanted to improve the requirement traceability and fulfilment.
* Help make planning decisions. Focusing the developer attention on specific aspects of development leads to better understanding of the problem and planning of the solution.
* Provide consistent way of stepwise development of mode and FT aspects by a notion of views refinement.

= Choices / Decisions =
= Available Documentation =
= Planning =

[[Category:D32 Deliverable]]