Setting up the modelling environment

This page describes the steps necessary to configure a fresh installation of SafeCap Platform to obtain a minimal modelling environment based on the results of the SafeCap Project. Other tool specialisations are possible and the following instruction only cover one specific scenario.

1. Import tool and pattern definitions

There is a schema verification tool based on the ProB model checker. The tool is made of two Epsilon scripts: an EGL script to transform a schema into a B model and and EOL script to interface with the model checker. At the moment, it is outdated and we are working on a more advanced version. It does demonstrate, however, the general approach to interface with external tools.

We also provide several examples of schema transformation patterns and capacity metrics. Again, these come in the form of Epsilon scripts and may be used as a starting point to define new patterns and scripts.

The import steps are:

• download a tool definitions file tools-0.2.zip;
• in the running platform, select File/Import and use option Existing Projects into Workspace;
• select the downloaded zip file and click Finish;
• the following projects will now appear in your workspace:
  • Capacity: capacity scipts;
  • Patterns: schema change patterns;
  • Verification: verification tool definitions;

2. Setup external tool paths

Script Verification/t_mc.eol depends on a local installation of ProB model checker. Make sure you have one installed on your computer and proceed as follows:

• in the platform, navigate to Window/Preferences or File/Preferences and locate Verification Tool Paths tab;
• add new tool with name prob and the path pointing at probcli executable of a ProB distribution;

3. Setup verification profiles

To run verification, a user needs to define at least one verification profile - a set of tools that are used together on a given schema. We show how to define a verification profile made of a single tool Verification/t_mc.eol; other tools may be added to this profile or additional profiles may be defined.

• navigate to Window/Preferences or File/Preferences and locate Verification Profiles tab;
• add a new profile, give it a name it pick some or all of the available tools;

From this point, the verification button may be used to launch any of the defined verification profiles. By default, it starts the last one used.

4. Import examples

You may find examples (railways junctions and perhaps some accompanying scripts) in the examples catalogue the official development website. Examples come in the form of a zip file and need to imported into the current workspace:

• select File/Import and use option Existing Projects into Workspace;
• select the example zip file and click Finish;
• example projects will appear in the workspace.