Event-B: Difference between revisions

ProB supports animation and model-checking for Event-B specifications.

Installation

To install the ProB plugin for Rodin, open the "Help" menu in Rodin and click "Install new software".

You see a drop-down list titled "Work with:" at the top of the install dialog. Choose the update site "ProB - ..." and click on "ProB for rodin2" in the field below. Click on the "Next" button at the button on the dialog and proceed with the installation as usual.

Alternativaly, one can use the Tcl/Tk version of ProB but Event-B models must be exported to an .eventb file first (see below).

Animation and Modelchecking

You can start animation of a model (machine or context) by right-clicking on the model in the Event-B explorer. Choose "Start Animation / Model Checking".

TODO: Here we should add more details about the ProB perspective and views.

Export for use with the Tcl/Tk version of ProB

You can export a model (machine or context) to an .eventb - file by right-clicking on the model in the Event-B explorer. You can find the corresponding menu item right below the animation item.

Such a .eventb file can be opened by the command line and Tcl/Tk version of ProB.

Theories

ProB has (limited) support for theories.

Currently supported are (examples refer to the theory project below):

• recursive datatypes (e.g. the List datatype)
• operators defined by direct definitions (e.g. operators in the BoolOps theory) or recursive definitions (e.g. operators in the List theory)
• special annotated operators (see below)

Axiomatically defined operators are not supported without additional annotations.

Tagging operators

ProB has some extra support for certain operators. ProB expects an annotation to an operator that provides the information that it should use a specific implementation for an operator. Such tags are given in a .ptm file (ProB Theory Mapping). The file must have the same name as the theory.

For each annotated operator, the file contains a line of the form

operator Name internal {Tag}

where Name is the name of the operator in the theory and Tag is a ProB internal name.

The use of these tags is usually for experts only. In the theory file below, some of the theories are annotated.

Currently are the following tags supported:

TODO: to be continued...

Download Theories

An example project with theories: media:theories2.zip theories2.zip

TODO: A description of the supported parts.