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

Flow diagram

The nodes of a flow diagram are events, possibly constrained with additional predicates; its edges are event relations. There are three kinds of event relations - enabling, disabling, feasibility. The event relations state the relationship between the after-state of one event and the enabling condition of the other. A flow diagram should not be confused with a state diagram or a workflow graph. The only effect of a flow diagram is the generation of additional verification; it has no behavioral semantics and does not constrain machine behaviour.

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