Difference between pages "Event-B Qualitative Probability User Guide" and "Event-B Statemachines"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Son
 
imported>Vitaly
 
Line 1: Line 1:
−
[[User:Son]] at '''ETH Zurich''' is in charge of the plug-in.
+
[[Image:IUMLB_big.png|frame|left]]
 
{{TOCright}}
 
{{TOCright}}
 +
==Overview==
  
−
== Introduction ==
+
Event-B Statemachines Plug-in is part of the iUML-B experimental tool that focuses on UML-B and Event-B integration. The plug-in provides a way of adding state machines directly to Event-B machines and is capable of translating former to Event-B language. It also offers a UML-like diagram editor for state machines, as well as state machine animation, which can be installed as additional plug-in that runs on top of ProB Animator.
−
Event-B Qualitative Probability plug-in provides supports for reasoning about termination with probability 1 (almost-certain termination).
 
  
 +
==Installation==
  
−
== Installing and Updating ==
+
The Event-B Statemachines plug-in is available for installation from Rodin update site under Modelling Extensions category. Animation plug-in for it is available from Verification and Validation category. Both plug-ins require EMF and GMF frameworks, Event-B EMF framework, ProB, OCL and QVT - all of these dependencies will be installed automatically upon plug-in installation.
−
The plug-in is available through the main Rodin Update Site under '''Modelling Extension''' category.
 
  
−
== News ==
+
==Using the tool==
−
* 23.11.2011: Version 0.2.1 released for Rodin 2.3.*
 
−
* 10.04.2012: Version 0.2.1 is compatible with Rodin 2.4.*
 
−
* 14.05.2012: Version 0.2.1 is compatible with Rodin 2.5.*
 
  
−
== Technical References ==
+
The tool consists of a standard UML-like graphical editor for state machine diagrams, an integration to Event-B Explorer and a translator to Event-B language. Some of these may seem familiar to you if you have experience with UML editors or UML-B plug-in for Rodin.
−
* S. Hallerstede, T.S. Hoang. '''Qualitative Probabilistic Modelling in Event-B'''. In ''IFM 2007: Integrated Formal Methods, 6th International Conference Proceedings'', Oxford, UK, July 2-5, 2007, volume 4591 of LNCS © Springer-Verlag. [http://dx.doi.org/10.1007/978-3-540-73210-5_16 Springer website]
 
−
** Initial idea about probabilistic convergence event.
 
−
** New modelling elements: Variant bound
 
−
** New proof obligations: '''PRV''', '''BND''', '''FINACT'''.
 
−
** Example: Resolve contention in IEEE 1395 (Firewire protocol).
 
  
−
* E. Yilmaz, T.S. Hoang. '''Development of Rabin’s Choice Coordination Algorithm in Event-B'''.  In ''Automated Verification of Critical Systems 2010'', volume 35 of ''Electronic Communications of the EASST'' © EASST. [http://journal.ub.tu-berlin.de/eceasst/article/view/548 EASST website]
+
===Event-B Explorer===
−
** Probablistic convergence event with refinement
 
−
** Constraints on how (not-) to refine probabilistic events.
 
−
** Example: Rabin's Choice Coordination Algorithm.
 
  
−
== Usage ==
+
[[Image:New_statemachine.png|thumbnail|State machine in Event-B Explorer]]
−
We illustrate the usage of the plug-in using the example of contention resolving (part of IEEE 1394 Firewire protocol). The description of the problem is as follows.
 
  
−
Two processes in contention use a probabilistic protocol to resolve the problem. In each step, each process probabilisitcally choose to communicate in either short or long delay.  The contention is resolved when the processes choose different delays.
+
To start the modelling all you have to do is to select a machine in Event-B Explorer that you would like to extend with state machines and click on ''Create new statemachine'' from explorer's toolbar. An input dialog will appear asking you for name of a new state machine. After that you should be able to see a new state machine appearing as a child of machine in explorer.
  
−
We start with a non-deterministic model of the system
+
The explorer also shows the contents of state machines, including states, transitions and annotations. You can customise the amount if information you would like to see by going to explorer's menu (a small triangle at the top right-hand side) ''> Customize View.. > Filters'' tab. There are three filters defined for state machines: ''Annotation Filter, Transition Filter, State Filter'' - that hide corresponding elements in explorer (state filter hides simple states, like initial, final or ANY).
−
* Boolean variables <math>x</math> and <math>y</math> represent the choice for each process: <math>TRUE</math> for short delay <math>FALSE</math> for long delay.
 
  
−
* Resolving contention is model as an event of the model with guard <math>x = y</math> (i.e. keep trying when the choices are identical).
+
In addition, there are ''Open'' and ''Delete'' actions available for state machine in context menu of explorer. These allow to open a state machine in editor (shortcut is double-click) and delete a state machine (shortcut is Delete key). In machine's context menu there are two more actions related to state machines: ''Refine with statemachines'' and ''Delete generated'' - which allow correspondingly to create a refinement of machine with state machine refinements (not available yet from standard ''Refine'' action of Rodin) and to delete all Event-B elements generated by state machines (required only for experimental purposes if generated things/diagrams get corrupted).
−
[[Image:contention-nondet.jpg]]
 
  
 +
===Diagram Editor===
  
−
=== Probabilistic Modelling ===
+
[[Image:Statemachine editor.png|thumbnail|left|State machine diagram editor]]
−
* To set event '''resolve''' is probabilistic convergence:
 
−
# Go to the '''Edit''' page of the standard ''Rodin Editor''.
 
−
# Open the '''EVENTS''' section
 
−
# Set convergence attribute of '''resolve''' from ''ordinary'' to ''convergent''.
 
−
# Set probabilistic attribute of '''resolve''' from ''standard'' to ''probabilistic''.
 
−
[[Image:contention-prob.jpg]]
 
  
−
* Set <math>\Bool \setminus \{x, y\}</math> as the variant of the model
+
To edit a state machine in diagram editor you simply double-click it. The tool creates a diagram file for you with the same name as root state machine.
−
[[Image:contention-variant.jpg]]
 
  
−
* Set <math>\Bool</math> as the bound of the model
+
Working with the editor is straightforward. The element creation tools are available from palette, divided into three categories: ''States'', ''State Features'' and ''State Links''. When a diagram element is selected on canvas the Properties View shows its available properties (if you cannot find it, please go to Rodin's menu ''Window > Show View > Properties''). After a state machine is complete it can be validated to make sure it has no semantic errors and translated to Event-B. When translated, it can be animated with ProB.
−
[[Image:contention-bound.jpg]]
 
  
−
* Save the model
 
  
−
=== Proof Obligations ===
 
−
* The model should have 3 proof obligations including '''resolve/PRV'''.
 
−
[[Image:contention-po.jpg]]
 
  
−
* The goal of proof obligation '''resolve/PRV''' is <math>\exists x^\prime, y^\prime \qdot \Bool \setminus \{x^\prime, y^\prime\} \subset \Bool \setminus \{x, y\}</math>.  With hypothesis <math>x = y</math> (from the guard of the event), the proof obligation can be discharged by instantiating different values for <math>x^\prime</math> and <math>y^\prime</math> (e.g. <math>\True</math> for <math>x^\prime</math> and <math>\False</math> for <math>y^\prime</math>). Alternatively, the obligation can be interactively discharge using '''p1''' (AterlierB Predicate Prover on lasso'd hypotheses) directly as shown below
 
−
[[Image:resolve-prv.jpg]]
 
  
−
== Explanations for some warning and error messages ==
 
  
−
* '''Missing variant''' warning
 
−
** Problem: [[Image:contention-novariant.jpg]]
 
−
** Explanation: User needs to provide a variant for probabilistic convergence events.
 
−
** Solution: Add a variant to the model
 
  
  
−
* '''Missing bound''' error
 
−
** Problem: [[Image:contention-nobound.jpg]]
 
−
** Explanation: The variant for probabilistic events need to be bounded above.
 
−
** Solution: Add a bound to the model (using Edit page of the standard Rodin editor).
 
  
−
== Additional features to be investigated/implemented ==
 
−
* ''Proof hints'': Select event guards when creating proof obligations, such as PRV and BND
 
  
−
* ''Finer-grain for probabilisitc attribute''. The probabilistic attribute might/should be attached to individual assignment and/or parameter of the event.
+
 
 +
====Elements====
 +
 
 +
The diagram allows to create the following ''State'' elements:
 +
* State
 +
* Refined State (shall not be used)
 +
* Initial (state)
 +
* Final (state)
 +
* ANY (state)
 +
Note: ANY-state is a convenience element for drawing local transitions which can also be drawn in a standard way - connecting parent state to its internal state.
 +
 
 +
A state can have nested state machines, added from ''State Features'', which correspond to UML parallel substates, also called parallel (or orthogonal) regions. As other features it may have invariants, which can also be theorems, and are defined as Event-B expression.
 +
 
 +
Finally, states can have transitions from one to another, created from ''State Links''. Transitions can also be created from popup arrows on states and link to either existing states or to ones created from the context menu.
 +
 
 +
====Semantics====
 +
 
 +
Listed elements, apart from refined versions (which are actually not intended for manual creation), are components of a standard UML state machine diagram notation. The semantics of Event-B state machines therefore compares to that of UML. Nevertheless, there is inevitable coupling between a state machine and Event-B which is important to consider during modelling.
 +
 
 +
State machines, states and transitions are integrated in Event-B machine and generate new elements in that machine upon translation:
 +
* States translate into boolean-typed variables (variable and type invariant)
 +
* State machines and states translate to their relationship invariants such as substate and partitioning invariant
 +
* Transitions and states translate to event guards and actions that describe state change behaviour
 +
 
 +
While state machines and states are not related to Event-B, for transitions it is necessary to know the events to which new guards and actions will be added. Thus a transition has an attribute called ''elaboration'' that links it to Event-B event. The relationship between two is rather flexible - a single transition can elaborate multiple events, and at the same time a single event can be elaborated by multiple transitions (you must be careful though not to misuse this feature).
 +
 
 +
State invariants is another Event-B aspect of state machine diagrams that has no connection with UML. Adding an invariant to a state will be interpreted in terms of Event-B as adding an invariant on state variable's value. State invariants are defined as Event-B expressions.
 +
 
 +
There are some semantic rules that must be obeyed in order for a state machine model to be valid and translatable to Event-B. These rules are implemented in the validation framework and are checked either when validation is called explicitly from context menu, or before the translation. Note that the set of rules is currently not complete thus not guaranteeing full correctness of the model.
 +
 
 +
[[Image:Statemachine markers.png|thumbnail|State machine error and warning markers]]
 +
 
 +
Rules:
 +
* Transition cannot go to initial state
 +
* Transition cannot go from final state
 +
* Transition cannot go directly from initial to final state
 +
* Transition should elaborate an event if
 +
** it is on the root state machine (its source/target belongs to root)
 +
** it is in nested state machine and not initial or final (its source/target is initial or final state)
 +
* Initial state should have outgoing transitions
 +
* Final state should have incoming transitions
 +
* Root state machine must have an initial state
 +
* State machine can only have one initial state
 +
* State machine can only have one final state
 +
* State machine must have an initial state if
 +
** its parent state has incoming transitions
 +
** it has outgoing local transitions (going from a state to parent state or ANY state)
 +
* Concrete state cannot contain refined state machines
 +
* Concrete state machine cannot have refined states
 +
* Refined state machine cannot have concrete states
 +
 
 +
Not all the rules are strict i.e. violation of certain rules is not considered as error as it doesn't cause translation problems, but keeping a model semantically correct means everything will be translated as intended.
 +
 
 +
The diagram editor, as mentioned, has two ways of checking the diagram model against these rules: selecting ''Validate'' from diagram context menu or running a translation. After validation completes, it produces feedback in the form of a dialog, telling whether model is valid or has errors. The elements that violate specific rules are marked with error/warning markers, which are listed in Rodin Problems view, as well as displayed on the diagram.
 +
 
 +
====Context Menu====
 +
 
 +
The context menu of a diagram includes four specific actions:
 +
* ''Validate'' - to run the validation check on state machine model
 +
* ''Translate to Event-B'' - to run the translation of a state machine to Event-B language
 +
* ''Start Animation'' - to run ProB animation and animate the diagram
 +
* ''Stop Animation'' - to stop the animation and return to Event-B perspective
 +
 
 +
===Known Problems===
 +
 
 +
The tool is at the experimental development stage and has some known, and likely some unknown issues. Amongst the former ones:
 +
* Renaming of machine or event causes existing diagrams to lose references to renamed element and thus become corrupted. Therefore it is recommended not to rename existing elements after you have created state machines.
 +
* Refinement of machine is refining contained state machines only if you use the custom action from context menu ''Refine with statemachines''. Standard Rodin refinement mechanism is not supporting yet (though planned in the nearest release) extensions and thus ignore any non-Rodin elements including state machines.
 +
* Refinement of state machines creates their refined versions in refined machine, but does not create corresponding diagram files. Thereby on opening a refined state machine a new diagram will be created with default layout, in other words the layout from abstract state machine diagram is not persisted in refinement.
 +
* Animation of state machine diagrams works only on a single diagram
 +
 
 +
[[Category:Plugin]] [[Category:User documentation]]

Revision as of 11:21, 18 May 2011

IUMLB big.png

Overview

Event-B Statemachines Plug-in is part of the iUML-B experimental tool that focuses on UML-B and Event-B integration. The plug-in provides a way of adding state machines directly to Event-B machines and is capable of translating former to Event-B language. It also offers a UML-like diagram editor for state machines, as well as state machine animation, which can be installed as additional plug-in that runs on top of ProB Animator.

Installation

The Event-B Statemachines plug-in is available for installation from Rodin update site under Modelling Extensions category. Animation plug-in for it is available from Verification and Validation category. Both plug-ins require EMF and GMF frameworks, Event-B EMF framework, ProB, OCL and QVT - all of these dependencies will be installed automatically upon plug-in installation.

Using the tool

The tool consists of a standard UML-like graphical editor for state machine diagrams, an integration to Event-B Explorer and a translator to Event-B language. Some of these may seem familiar to you if you have experience with UML editors or UML-B plug-in for Rodin.

Event-B Explorer

State machine in Event-B Explorer

To start the modelling all you have to do is to select a machine in Event-B Explorer that you would like to extend with state machines and click on Create new statemachine from explorer's toolbar. An input dialog will appear asking you for name of a new state machine. After that you should be able to see a new state machine appearing as a child of machine in explorer.

The explorer also shows the contents of state machines, including states, transitions and annotations. You can customise the amount if information you would like to see by going to explorer's menu (a small triangle at the top right-hand side) > Customize View.. > Filters tab. There are three filters defined for state machines: Annotation Filter, Transition Filter, State Filter - that hide corresponding elements in explorer (state filter hides simple states, like initial, final or ANY).

In addition, there are Open and Delete actions available for state machine in context menu of explorer. These allow to open a state machine in editor (shortcut is double-click) and delete a state machine (shortcut is Delete key). In machine's context menu there are two more actions related to state machines: Refine with statemachines and Delete generated - which allow correspondingly to create a refinement of machine with state machine refinements (not available yet from standard Refine action of Rodin) and to delete all Event-B elements generated by state machines (required only for experimental purposes if generated things/diagrams get corrupted).

Diagram Editor

State machine diagram editor

To edit a state machine in diagram editor you simply double-click it. The tool creates a diagram file for you with the same name as root state machine.

Working with the editor is straightforward. The element creation tools are available from palette, divided into three categories: States, State Features and State Links. When a diagram element is selected on canvas the Properties View shows its available properties (if you cannot find it, please go to Rodin's menu Window > Show View > Properties). After a state machine is complete it can be validated to make sure it has no semantic errors and translated to Event-B. When translated, it can be animated with ProB.






Elements

The diagram allows to create the following State elements:

  • State
  • Refined State (shall not be used)
  • Initial (state)
  • Final (state)
  • ANY (state)

Note: ANY-state is a convenience element for drawing local transitions which can also be drawn in a standard way - connecting parent state to its internal state.

A state can have nested state machines, added from State Features, which correspond to UML parallel substates, also called parallel (or orthogonal) regions. As other features it may have invariants, which can also be theorems, and are defined as Event-B expression.

Finally, states can have transitions from one to another, created from State Links. Transitions can also be created from popup arrows on states and link to either existing states or to ones created from the context menu.

Semantics

Listed elements, apart from refined versions (which are actually not intended for manual creation), are components of a standard UML state machine diagram notation. The semantics of Event-B state machines therefore compares to that of UML. Nevertheless, there is inevitable coupling between a state machine and Event-B which is important to consider during modelling.

State machines, states and transitions are integrated in Event-B machine and generate new elements in that machine upon translation:

  • States translate into boolean-typed variables (variable and type invariant)
  • State machines and states translate to their relationship invariants such as substate and partitioning invariant
  • Transitions and states translate to event guards and actions that describe state change behaviour

While state machines and states are not related to Event-B, for transitions it is necessary to know the events to which new guards and actions will be added. Thus a transition has an attribute called elaboration that links it to Event-B event. The relationship between two is rather flexible - a single transition can elaborate multiple events, and at the same time a single event can be elaborated by multiple transitions (you must be careful though not to misuse this feature).

State invariants is another Event-B aspect of state machine diagrams that has no connection with UML. Adding an invariant to a state will be interpreted in terms of Event-B as adding an invariant on state variable's value. State invariants are defined as Event-B expressions.

There are some semantic rules that must be obeyed in order for a state machine model to be valid and translatable to Event-B. These rules are implemented in the validation framework and are checked either when validation is called explicitly from context menu, or before the translation. Note that the set of rules is currently not complete thus not guaranteeing full correctness of the model.

State machine error and warning markers

Rules:

  • Transition cannot go to initial state
  • Transition cannot go from final state
  • Transition cannot go directly from initial to final state
  • Transition should elaborate an event if
    • it is on the root state machine (its source/target belongs to root)
    • it is in nested state machine and not initial or final (its source/target is initial or final state)
  • Initial state should have outgoing transitions
  • Final state should have incoming transitions
  • Root state machine must have an initial state
  • State machine can only have one initial state
  • State machine can only have one final state
  • State machine must have an initial state if
    • its parent state has incoming transitions
    • it has outgoing local transitions (going from a state to parent state or ANY state)
  • Concrete state cannot contain refined state machines
  • Concrete state machine cannot have refined states
  • Refined state machine cannot have concrete states

Not all the rules are strict i.e. violation of certain rules is not considered as error as it doesn't cause translation problems, but keeping a model semantically correct means everything will be translated as intended.

The diagram editor, as mentioned, has two ways of checking the diagram model against these rules: selecting Validate from diagram context menu or running a translation. After validation completes, it produces feedback in the form of a dialog, telling whether model is valid or has errors. The elements that violate specific rules are marked with error/warning markers, which are listed in Rodin Problems view, as well as displayed on the diagram.

Context Menu

The context menu of a diagram includes four specific actions:

  • Validate - to run the validation check on state machine model
  • Translate to Event-B - to run the translation of a state machine to Event-B language
  • Start Animation - to run ProB animation and animate the diagram
  • Stop Animation - to stop the animation and return to Event-B perspective

Known Problems

The tool is at the experimental development stage and has some known, and likely some unknown issues. Amongst the former ones:

  • Renaming of machine or event causes existing diagrams to lose references to renamed element and thus become corrupted. Therefore it is recommended not to rename existing elements after you have created state machines.
  • Refinement of machine is refining contained state machines only if you use the custom action from context menu Refine with statemachines. Standard Rodin refinement mechanism is not supporting yet (though planned in the nearest release) extensions and thus ignore any non-Rodin elements including state machines.
  • Refinement of state machines creates their refined versions in refined machine, but does not create corresponding diagram files. Thereby on opening a refined state machine a new diagram will be created with default layout, in other words the layout from abstract state machine diagram is not persisted in refinement.
  • Animation of state machine diagrams works only on a single diagram
Retrieved from ‘https://wiki.event-b.org/index.php?title=Event-B_Qualitative_Probability_User_Guide&oldid=4254’