Flows

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.

Sample flow diagram

Update site

Use the following update site to install and update the plug in.

http://iliasov.org/usecase

See also

Old Flow Plug in page