Flows: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Alexili mNo edit summary |
imported>Alexili mNo edit summary |
||
| 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
