Difference between revisions of "Flows"
From Event-B
Jump to navigationJump to searchimported>Alexili m |
imported>Alexili m |
||
| Line 1: | Line 1: | ||
| − | + | The Flow plug in is a Rodin Platform extension assisting in the formulation of verification conditions related to the dynamic properties of a model, i.e., event ordering and enabledness conditions. A visual notation is used to define graph-like structures that are translated into Event-B theorems (for efficiency reasons, these appear as machine proof obligations). The tool simplifies a number of routine tasks such as writing and maintaining deadlock-freedom and relative deadlock freedom proof obligations. Its core functionality is concerned with the verification of the feasibility of use case scenarious: checking that a given event paths are feasible in a given model. | |
| − | |||
| − | |||
| + | [[Image:Flow_doors.png|thumb|right|Sample flow diagram]] | ||
==== Update site ==== | ==== Update site ==== | ||
Revision as of 02:36, 22 January 2011
The Flow plug in is a Rodin Platform extension assisting in the formulation of verification conditions related to the dynamic properties of a model, i.e., event ordering and enabledness conditions. A visual notation is used to define graph-like structures that are translated into Event-B theorems (for efficiency reasons, these appear as machine proof obligations). The tool simplifies a number of routine tasks such as writing and maintaining deadlock-freedom and relative deadlock freedom proof obligations. Its core functionality is concerned with the verification of the feasibility of use case scenarious: checking that a given event paths are feasible in a given model.
Update site
Use the following update site to install and update the plug in.
http://iliasov.org/usecase
