D23 Flow Plug-in - Revision history

imported>Pascal: /* Available Documentation */

2010-01-08T11:37:09Z

Available Documentation

← Older revision		Revision as of 11:37, 8 January 2010
Line 30:		Line 30:
	= Available Documentation =		= Available Documentation =

	There is a [[Flows\|wiki]] page summarising proof obligation involved in proving machine/flow consistency.		There is a [http://wiki.event-b.org/index.php/Flows wiki] page summarising proof obligation involved in proving machine/flow consistency.

	= Planning =		= Planning =

imported>Tommy: /* Choices / Decisions */

2009-12-10T15:51:56Z

Choices / Decisions

← Older revision		Revision as of 15:51, 10 December 2009
Line 26:		Line 26:
	The primary functionality of the plug-in is the generation of additional proof obligations. Rodin model builder automatically invokes the static checker and the proof obligations generator of the plug-in and the proof obligations related to flow appear in the list of the model proof obligations.		The primary functionality of the plug-in is the generation of additional proof obligations. Rodin model builder automatically invokes the static checker and the proof obligations generator of the plug-in and the proof obligations related to flow appear in the list of the model proof obligations.

	One of the lessons learned with an initial plug-in prototype was that a CSP-like language notation is not the best way to express event ordering as not all users are familiar with process algebraic notations. It was decided to use graphical editor to ~~would~~ allow a visual layout of flow diagrams. This, in our view, is a more intuitive way of specifying event ordering. To realise this, we have relied on GMF - an Eclipse library to manipulate EMF models using graphical editors.		One of the lessons learned with an initial plug-in prototype was that a CSP-like language notation is not the best way to express event ordering as not all users are familiar with process algebraic notations. It was decided to use graphical editor to allow a visual layout of flow diagrams. This, in our view, is a more intuitive way of specifying event ordering. To realise this, we have relied on GMF - an Eclipse library to manipulate EMF models using graphical editors.

	= Available Documentation =		= Available Documentation =

imported>Tommy: /* Choices / Decisions */

2009-12-10T15:49:51Z

Choices / Decisions

← Older revision		Revision as of 15:49, 10 December 2009
Line 26:		Line 26:
	The primary functionality of the plug-in is the generation of additional proof obligations. Rodin model builder automatically invokes the static checker and the proof obligations generator of the plug-in and the proof obligations related to flow appear in the list of the model proof obligations.		The primary functionality of the plug-in is the generation of additional proof obligations. Rodin model builder automatically invokes the static checker and the proof obligations generator of the plug-in and the proof obligations related to flow appear in the list of the model proof obligations.

	One of the lessons learned with an initial plug-in prototype was that a CSP-like language notation is not the best way to express event ordering as not all users are ~~not~~ familiar with process algebraic notations. It was decided to use graphical editor to would allow a visual layout of flow diagrams. This, in our view, is a more intuitive way of specifying event ordering. To realise this, we have relied on GMF - an Eclipse library to manipulate EMF models using graphical editors.		One of the lessons learned with an initial plug-in prototype was that a CSP-like language notation is not the best way to express event ordering as not all users are familiar with process algebraic notations. It was decided to use graphical editor to would allow a visual layout of flow diagrams. This, in our view, is a more intuitive way of specifying event ordering. To realise this, we have relied on GMF - an Eclipse library to manipulate EMF models using graphical editors.

	= Available Documentation =		= Available Documentation =

imported>Pascal: /* Typos */

2009-12-04T11:26:27Z

Typos

imported>Alexili at 12:54, 30 November 2009

2009-11-30T12:54:46Z

← Older revision		Revision as of 12:54, 30 November 2009
Line 8:		Line 8:
	* event may follow an event; this is the weakest form of connection when we only say that it may be the case that the second event follows the first event; it may happen, however, that some other event interferes and the second event is delayed or is even not enabled ever.		* event may follow an event; this is the weakest form of connection when we only say that it may be the case that the second event follows the first event; it may happen, however, that some other event interferes and the second event is delayed or is even not enabled ever.

	Although the last case may seem the least appealing, it is the one that forms the basis of the Flows plugin. The primary reason for offering such a weak guarantee is proof effort required for stronger types of connectives~~. Let us see what it means to provide a formal proof for the various cases of sequential event composition~~.		Although the last case may seem the least appealing, it is the one that forms the basis of the Flows plugin. The primary reason for offering such a weak guarantee is proof effort required for stronger types of connectives.

	= Motivations =		= Motivations =
Line 24:		Line 24:
	= Choices / Decisions =		= Choices / Decisions =

			The primary functionality of the plugin is the generation of additional proof obligations. Rodin model builder automatically invokes the static checker and the proof obligations generator of the plugin and the proof obligations related to flow appear in the list of the model proof obligations.

			One of the lessons learned with an initial plugin prototype was that a CSP-like language notation is not the best way to express event ordering as not all users are not familiar with process algebraic notations. It was decided to use graphical editor to would allow a visual layout of flow diagrams. This, in our view, is a more intuitive way of specifying event ordering. To realise this, we have relied on GMF: an Eclipse library for manipulating EMF models using graphical editors.

	= Available Documentation =		= Available Documentation =

			There is a [[Flows\|wiki]] page summarising proof obligation involved in proving machine/flow consistency.

	= Planning =		= Planning =

imported>Alexili: New page: = Overview = Event-B, being an event systems formalism does not have a mechanism for explicitly defining event ordering. Although event guards may express any desired event ordering, the ...

2009-11-30T12:41:54Z

New page: = Overview = Event-B, being an event systems formalism does not have a mechanism for explicitly defining event ordering. Although event guards may express any desired event ordering, the ...

New page

= Overview =

Event-B, being an event systems formalism does not have a mechanism for explicitly defining event ordering. Although event guards may express any desired event ordering, the ability to have a summary of possible event flows in a concise and compact form is useful for many tasks, for example, code generation and connecting with other formalisms. The flows plugin addresses one aspect of event ordering: it allows a modeller to specify and prove that a given sequence of events does not contradict a given machine specification. More precisely, if we were to execute a machine step-by-step following our prescribed sequence of events we would not discover divergencies and deadlocks not already present in the original machine. In other words, the constraining of event ordering must be such that the overall specification is an Event-B refinement of the original model. Importantly, this means that all the desired model properties proved before are preserved.

Sequential composition of events may be expressed in a number of ways:
* event immediately follows another event; no other events may take place between the composed events.
* event eventually follows an event; thus, although there is an interference from other events, it is guaranteed that the second is eventually enabled.
* event may follow an event; this is the weakest form of connection when we only say that it may be the case that the second event follows the first event; it may happen, however, that some other event interferes and the second event is delayed or is even not enabled ever.

Although the last case may seem the least appealing, it is the one that forms the basis of the Flows plugin. The primary reason for offering such a weak guarantee is proof effort required for stronger types of connectives. Let us see what it means to provide a formal proof for the various cases of sequential event composition.

= Motivations =

There are a number of reasons to consider an extension of Event-B with an event ordering mechanism:
* for some problems the information about event ordering is an essential part of requirements; it comes as a natural expectation to be able to adequately reproduce these in a model;
* explicit control flow may help in proving properties related to event ordering;
* sequential code generation requires some form of control flow information;
* since event ordering could restrict the non-determinism in event selection, model checking is likely to be more efficient for a composition of a machine with event ordering information;
* a potential for a visual presentation based on control flow information;
* bridging the gap between high-level workflow and architectural languages, and Event-B.

It is also hoped that the plugin would improve readability of larger models: currently they are simply a long list of events with nothing except comments to provide any structuring clues.

= Choices / Decisions =

= Available Documentation =

= Planning =
The plugin is to be available for the time of release of Platform version 1.2.

[[Category:D23 Deliverable]]

← Older revision		Revision as of 11:26, 4 December 2009
Line 1:		Line 1:
	= Overview =		= Overview =

	Event-B, being an event systems formalism does not have a mechanism ~~for~~ explicitly ~~defining~~ event ordering. Although event guards may express any desired event ordering, the ability to have a summary of possible event flows in a concise and compact form is useful for many tasks, for example, code generation and connecting with other formalisms. The flows ~~plugin~~ addresses one aspect of event ordering: it allows a modeller to specify and prove that a given sequence of events does not contradict a given machine specification. More precisely, if we were to execute a machine step-by-step following our prescribed sequence of events we would not discover ~~divergencies~~ and deadlocks not already present in the original machine. In other words, the ~~constraining of~~ event ordering must be such that the overall specification is an Event-B refinement of the original model. Importantly, this means that all the desired model properties proved before are preserved.		Event-B, being an event systems formalism, does not have a mechanism to explicitly define event ordering. Although event guards may express any desired event ordering, the ability to have a summary of possible event flows in a concise and compact form is useful for many tasks, for example, code generation and connecting with other formalisms. The flows plug-in addresses one aspect of event ordering: it allows a modeller to specify and prove that a given sequence of events does not contradict a given machine specification. More precisely, if we were to execute a machine step-by-step following our prescribed sequence of events we would not discover divergences and deadlocks not already present in the original machine. In other words, the constraint on event ordering must be such that the overall specification is an Event-B refinement of the original model. Importantly, this means that all the desired model properties proved before are preserved.

	Sequential composition of events may be expressed in a number of ways:		Sequential composition of events may be expressed in a number of ways:
	* ~~event~~ immediately follows another event; no other events may take place between the composed events.		* Event immediately follows another event; no other events may take place between the composed events.
	* ~~event~~ eventually follows an event; thus, although there is an interference from other events, it is guaranteed that the second is eventually enabled.		* Event eventually follows an event; thus, although there is an interference from other events, it is guaranteed that the second is eventually enabled.
	* ~~event~~ may follow an event; this is the weakest form of connection when we only say that it may be the case that the second event follows the first event; it may happen, however, that some other event interferes and the second event is delayed or is even not enabled ever.		* Event may follow an event; this is the weakest form of connection when we only say that it may be the case that the second event follows the first event; it may happen, however, that some other event interferes and the second event is delayed or is even not enabled ever.

	Although the last case may seem the least appealing, it is the one that forms the basis of the Flows ~~plugin~~. The primary reason ~~for offering~~ such a weak guarantee is proof effort required for stronger types of connectives.		Although the last case may seem the least appealing, it is the one that forms the basis of the Flows plug-in. The primary reason to offer such a weak guarantee is proof effort required for stronger types of connectives.

	= Motivations =		= Motivations =

	There are a number of reasons to consider an extension of Event-B with an event ordering mechanism:		There are a number of reasons to consider an extension of Event-B with an event ordering mechanism:
	* ~~for~~ some problems the information about event ordering is an essential part of requirements; it comes as a natural expectation to be able to adequately reproduce these in a model;		* For some problems the information about event ordering is an essential part of requirements; it comes as a natural expectation to be able to adequately reproduce these in a model.
	* ~~explicit~~ control flow may help in proving properties related to event ordering;		* Explicit control flow may help in proving properties related to event ordering.
	* ~~sequential~~ code generation requires some form of control flow information;		* Sequential code generation requires some form of control flow information.
	* ~~since~~ event ordering could restrict the non-determinism in event selection, model checking is likely to be more efficient for a composition of a machine with event ordering information;		* Since event ordering could restrict the non-determinism in event selection, model checking is likely to be more efficient for a composition of a machine with event ordering information.
	* a potential for a visual presentation based on control flow information;		* A potential for a visual presentation based on control flow information.
	* ~~bridging~~ the gap between high-level workflow and architectural languages, and Event-B.		* Bridging the gap between high-level workflow and architectural languages, and Event-B.

	It is also hoped that the ~~plugin~~ would improve readability of larger models: currently they are simply a long list of events with nothing except comments to provide any structuring clues.		It is also hoped that the plug-in would improve readability of larger models: currently they are simply a long list of events with nothing except comments to provide any structuring clues.

	= Choices / Decisions =		= Choices / Decisions =

	The primary functionality of the ~~plugin~~ is the generation of additional proof obligations. Rodin model builder automatically invokes the static checker and the proof obligations generator of the ~~plugin~~ and the proof obligations related to flow appear in the list of the model proof obligations.		The primary functionality of the plug-in is the generation of additional proof obligations. Rodin model builder automatically invokes the static checker and the proof obligations generator of the plug-in and the proof obligations related to flow appear in the list of the model proof obligations.

	One of the lessons learned with an initial ~~plugin~~ prototype was that a CSP-like language notation is not the best way to express event ordering as not all users are not familiar with process algebraic notations. It was decided to use graphical editor to would allow a visual layout of flow diagrams. This, in our view, is a more intuitive way of specifying event ordering. To realise this, we have relied on GMF: an Eclipse library ~~for manipulating~~ EMF models using graphical editors.		One of the lessons learned with an initial plug-in prototype was that a CSP-like language notation is not the best way to express event ordering as not all users are not familiar with process algebraic notations. It was decided to use graphical editor to would allow a visual layout of flow diagrams. This, in our view, is a more intuitive way of specifying event ordering. To realise this, we have relied on GMF - an Eclipse library to manipulate EMF models using graphical editors.

	= Available Documentation =		= Available Documentation =
Line 33:		Line 33:

	= Planning =		= Planning =
	The ~~plugin~~ is ~~to be~~ available ~~for~~ the ~~time of~~ release ~~of Platform version~~ 1.2.		The plug-in is available since the release 1.2 of the platform.

	[[Category:D23 Deliverable]]		[[Category:D23 Deliverable]]