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.
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.
Enabling relation
The enabling relation expresses that an event may follow some other event. More precisely, it requires that the guard of the event at the target of the relation edge is enabled after the execution of the event at the source of the edge. It is not guaranteed that the target event is executed immediately or eventually after the source event. The interference from other events may temporarily or permanently disable the target event even though it was momentarily enabled in the after-state of the first event. Below is an example of a flow diagram using the enabling relation.
Circle denotes the initialisation event; circle with a block dot is an implicit termination (or deadlock) event. The latter is defined as event with no actions and a guard formed by negating of the disjunction of the guards of all the model events (not including skip, initialisation and the termination events).
When for a node there is more than one outgoing relation of a given kind it is enough to satisfy any one of the relations. For the enabling relation, this expresses the internal choice on event firings. There are annotations, discussed further, overriding this interpretation.
Update site
Use the following update site to install and update the plug in.
http://iliasov.org/usecase
