Difference between pages "Modularisation Plug-in Release Notes" and "Modularisation Plug-in Tutorial"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Alexili
 
imported>Alexili
(New page: ==Modularisation Plug-in Tutorial== The tutorial illustrates the use of the modularisation plug-in in an Event-B development. The example used is rather small scale but it still demonstra...)
 
Line 1: Line 1:
 +
==Modularisation Plug-in Tutorial==
  
===Version 1.0.2 Changes===
+
The tutorial illustrates the use of the modularisation plug-in in an Event-B development. The example used is rather small scale but it still demonstrates some basic principles of introducing modules during the development process.
  
* Fixed the problem with having multiple operation postconditions constraining the same primed variable
+
===Sluice Control Example===
* Parallel assignment due a duplicate call is now handled gracefully
 
* New static checker rule to ensure that implementation events are either convergent or anticipated
 
* "Entry" flag in implementation is now called "final"
 
* Witnesses for operation parameters may now be used in an implementation machine. It is working but not very refined: once "final" flag is set on an event and machine is saved, a refinement clause appears in the event. It is a generated element that in future platform version would not be alterable. Normally,a machine would have to be touched and saved again for any existing problems related to witnesses to disappear.
 
  
===Version 1.0.1 Changes===
+
The example is a sluice with two doors connecting areas with dramatically different pressures. The pressure difference makes it unsafe to open a door unless the pressure is leveled between the areas connected by the door. The purpose of the system is to adjust the pressure in the sluice area and control the door locks to allow a user to get safely inside to outside. Such system can be deployed, for example, on a submarine to allow divers to get out while submerged.  
  
* Fixed a vicious bug that may lead to infinite loop in static checker.
+
The system parts are two doors that can be operated independently of each other and a pressure controller that allows the change of pressure in the sluice area. The following is a schematic depiction of the system.
* Fixed bug in operation precondition POG that prevented generation of POs for operations with parameters.
 
* Added operation invariant satisfaction PO.
 
* Added interface pretty printer.
 
 
Dealing with refinement:
 
* The "Refine" command available from a pop-up menu of the project explorer construct an initial refinement machine that does not declare the variables imported from modules. This typically results in a number of error messages saying that a variable is not declared. The problem is solved by adding the missing declarations manually.  
 
 
  
===Version 1.0.1 Release notes===
+
[[Image:SluiceController.png]]
 
General:
 
* Many necessary static checks are not implemented. It means that it is possible to run into troubles without getting any hint on what is happening. Some such checks are planned and many more are still to be discovered.
 
* Machine pretty printer is not aware of the extensions contributed by the plugin. Thus, all the additional elements, accessible in the composite editor, do not show up at all during pretty printing.
 
* The same problem as the above for the text editor.
 
* The plug-in cannot work alongside any other plug-in contributing SC and POG modules. It will try to override the current configuration of a component whenever a plug-in specific model element is updated. 
 
* Interface change is not automatically reacted upon by components depending on it - there is no proper dependency link. This is particularly problematic when cleaning and rebuilding a project.
 
  
Interface components:
+
The system is summarised with the following set of requirements:
* There is a bug in showing interface proof obligations - these are not refreshed automtically in the project explorer. To refresh the view, change a model part and save the model (e.g., type a comment)
+
# the system allows a user to get inside or outside by leveling pressure between room and a destination
* Interface variables do not have an initialisation. This results in a warning by a SC that cannot be addressed by a user.
+
# the system has three locations - ''outside'', ''sluice'' and ''inside''
* Currently, postconditions must be written in such a way that no two postconditions mention the same primed variable. The violation of this rule would result in a broken statically checked interface component.
+
# the system has two doors - ''door1'', connecting ''outside'' and ''sluice'', and ''door2'', connecting ''sluice'' and ''inside'';
* Operations without return variables are not supported. This is related to the fact that, for now, an operation call is always an expression rather than a predicate or a complete action.
+
# there is a device to change pressure in ''sluice'';
* There is no interface pretty-printer.
+
# a door may be opened only if the pressures in the locations it connects is equalised;
 
+
# at most one door is open at any moment;
Implementation machines:  
+
# the pressure can only be switched on when the doors are closed.
* It is not checked yet that all the interface operations are implemented.
 
* No proof obligations are generated to ensure deadlock freeness of event groups realising interface operations.
 
 
 
Interface import:
 
* There is no support for instantiation of given sets in imported interfaces. Set instantiation could be used to configure generic components to specific data types (or typing expressions) used in a main model.   
 
* New axioms (under the PROPERTIES section of USES) added while importing an interface are not validated in any manner except type checking.
 
* Operation call precondition proof obligation does not select the relevant hypothesis. Also, its hypothesis include event action hypothesis that should not be the cases for the obligation.
 
 
 
[[Category:Plugin]]
 

Revision as of 12:54, 22 October 2009

Modularisation Plug-in Tutorial

The tutorial illustrates the use of the modularisation plug-in in an Event-B development. The example used is rather small scale but it still demonstrates some basic principles of introducing modules during the development process.

Sluice Control Example

The example is a sluice with two doors connecting areas with dramatically different pressures. The pressure difference makes it unsafe to open a door unless the pressure is leveled between the areas connected by the door. The purpose of the system is to adjust the pressure in the sluice area and control the door locks to allow a user to get safely inside to outside. Such system can be deployed, for example, on a submarine to allow divers to get out while submerged.

The system parts are two doors that can be operated independently of each other and a pressure controller that allows the change of pressure in the sluice area. The following is a schematic depiction of the system.

SluiceController.png

The system is summarised with the following set of requirements:

  1. the system allows a user to get inside or outside by leveling pressure between room and a destination
  2. the system has three locations - outside, sluice and inside
  3. the system has two doors - door1, connecting outside and sluice, and door2, connecting sluice and inside;
  4. there is a device to change pressure in sluice;
  5. a door may be opened only if the pressures in the locations it connects is equalised;
  6. at most one door is open at any moment;
  7. the pressure can only be switched on when the doors are closed.