Group refinement plugin - Revision history

imported>Alexili at 15:33, 31 August 2010

2010-08-31T15:33:48Z

← Older revision		Revision as of 15:33, 31 August 2010
Line 65:		Line 65:
	* swap3: none		* swap3: none

			=== Bugs ===
			* witness warning: the plugin does not contribute static checker rules and thus a missing parameter in one of a group refinement events would make the static checker to complain about missing witness
	[[Category:Plugin]]		[[Category:Plugin]]

imported>Alexili at 13:33, 17 August 2010

2010-08-17T13:33:13Z

← Older revision		Revision as of 13:33, 17 August 2010
Line 35:		Line 35:

	Now you should have the plugin up and running. To start using the plugin, select a refinement machine in the Project Explorer, right-click to open a pop-up menu. At the bottom there should be two new menu items: ''Normal profile'' and ''Group profile''. These options control the current style of refinement lass. The normal profile stands for the standard set fo refinement laws. The group profile activates the additional laws for event group refinement.		Now you should have the plugin up and running. To start using the plugin, select a refinement machine in the Project Explorer, right-click to open a pop-up menu. At the bottom there should be two new menu items: ''Normal profile'' and ''Group profile''. These options control the current style of refinement lass. The normal profile stands for the standard set fo refinement laws. The group profile activates the additional laws for event group refinement.

			=== Proof Obligations ===

			(todo)

			=== Event Ordering Constraints ===

			In a general case, not all concrete event traces realise a valid refinement of an abstract event. For instance, in the example given above, it necessary to ensure that swap1 takes place before swap2 and, in its turn, swap2 before swap3. One solution is to count the step as it is done in the model with program counter ''pc''. The plugin, however, offers a more elegant mechanism of removing unwanted traces.

			To indicate the required event ordering a modeller should provide event ordering constraining expressions. These are places in the comments next to event declarations (in the text editor such comments is placed between ''event ce'' and ''refines ae''). The plugin will know that it is an event constrainign expression by seeing double square brackets, e.g., <nowiki>[[</nowiki>''first''<nowiki>]]</nowiki>. Everything placed within such brackets is considered to be a constraining expressions. No other characters should be placed on the same line before or after brackets (normall comment may follow or precede on other lines in a multi-line comment).

			The syntax is following. There are just four keywords: '''first''', '''next''', '''last''' and '''or'''. A constraining expression takes one of the following forms:
			* '''first''': the corresponding event is the first event in the trace
			* '''last''': the event is the last event in the trace
			* '''next''' ''event'' ('''or''' ''event'')*: the event is followed by a given list of events

			In addition, several expressions may be combined with single [[..]] brackets by separating with a semicolon (;). For example
			first; next ev1

			states that a given event is first and the next event is ''ev1''. Expression

			next ev1 or ev2

			means that the current event may be followed events ''ev1'' or ''ev2''.

			In the example given above, machine ''m1b'' has the following event constraining expressions:
			* swap1: <tt><nowiki>[[</nowiki>first; next swap2<nowiki>]]</nowiki></tt>
			* swap2: none
			* swap3: none

	[[Category:Plugin]]		[[Category:Plugin]]

imported>Alexei at 14:47, 16 August 2010

2010-08-16T14:47:49Z

← Older revision		Revision as of 14:47, 16 August 2010
Line 1:		Line 1:
	~~== Group refinement ==~~

	=== Motivation ===		=== Motivation ===

imported>Alexei at 14:31, 16 August 2010

2010-08-16T14:31:58Z

@@ Line 7: / Line 7: @@
 The group refinement plugin modifies the set of refinement laws within a scope of a single refinement step to remove the need for a housekeeping event. It also simplifies the concrete behaviour specification by allowing a user to forgo the variables and invariants necessary to link abstract and concrete behaviour. The intention is not to replace or remove any of the existing refinement laws but rather augment them with a new set of laws to make the overall refinement process more flexible.
-[[Abstract.png]]
+[[Image:Abstract.png]]
 One case where one would have to rely on a housekeeping event is the introduction of a loop. In this case, a housekeeping event forces to a modeller to provide a condition summarising the cumulative loop effect which is likely to be more amenable to analysis that a straightforward next-state relation closure.

imported>Alexei at 14:21, 16 August 2010

2010-08-16T14:21:08Z

← Older revision		Revision as of 14:21, 16 August 2010
Line 7:		Line 7:
	The group refinement plugin modifies the set of refinement laws within a scope of a single refinement step to remove the need for a housekeeping event. It also simplifies the concrete behaviour specification by allowing a user to forgo the variables and invariants necessary to link abstract and concrete behaviour. The intention is not to replace or remove any of the existing refinement laws but rather augment them with a new set of laws to make the overall refinement process more flexible.		The group refinement plugin modifies the set of refinement laws within a scope of a single refinement step to remove the need for a housekeeping event. It also simplifies the concrete behaviour specification by allowing a user to forgo the variables and invariants necessary to link abstract and concrete behaviour. The intention is not to replace or remove any of the existing refinement laws but rather augment them with a new set of laws to make the overall refinement process more flexible.


			[[Abstract.png]]

	One case where one would have to rely on a housekeeping event is the introduction of a loop. In this case, a housekeeping event forces to a modeller to provide a condition summarising the cumulative loop effect which is likely to be more amenable to analysis that a straightforward next-state relation closure.		One case where one would have to rely on a housekeeping event is the introduction of a loop. In this case, a housekeeping event forces to a modeller to provide a condition summarising the cumulative loop effect which is likely to be more amenable to analysis that a straightforward next-state relation closure.

imported>Alexei: New page: == Group refinement == === Motivation === According to the Event B refinement laws, new behaviour is introduced by adding new events to a refinement machine. Such new behaviour may corre...

2010-08-16T14:17:56Z

New page: == Group refinement == === Motivation === According to the Event B refinement laws, new behaviour is introduced by adding new events to a refinement machine. Such new behaviour may corre...

New page

== Group refinement ==

=== Motivation ===

According to the Event B refinement laws, new behaviour is introduced by adding new events to a refinement machine. Such new behaviour may correspond to a detalised description of some abstract behaviour especially when a previously atomic state transition has to be explained as a chain of state transitions. To satisfy the refinement relation, new events are only allowed to update new variables. New variables of a machine denote the part of a system state that is not mapped into the state of the abstract system, that is, they characterise a hidden state of a refined system. Since new events cannot be directly related to the abstract behaviour it is necessary to have a housekeeping event that would link the behaviour expressed on the hidden state with the refined abstract behaviour. Since a housekeeping event assigns to abstract variables that are to be ignored at the implementation stage it is clear that a housekeeping event does not contribute to the specification of the system behaviour. In fact, one should see not as a part of a concrete specification but rather an artefact of the refinement relation proof. Confusingly, Event-B does not make a distinction between abstract variables and events retained solely for the needs of the refinement proof and those preserved as an integral part of an overall specification in the incremental development process.

The group refinement plugin modifies the set of refinement laws within a scope of a single refinement step to remove the need for a housekeeping event. It also simplifies the concrete behaviour specification by allowing a user to forgo the variables and invariants necessary to link abstract and concrete behaviour. The intention is not to replace or remove any of the existing refinement laws but rather augment them with a new set of laws to make the overall refinement process more flexible.

One case where one would have to rely on a housekeeping event is the introduction of a loop. In this case, a housekeeping event forces to a modeller to provide a condition summarising the cumulative loop effect which is likely to be more amenable to analysis that a straightforward next-state relation closure.