ParTraP Toolset User Guide

We present ParTraP and its associated toolset, supporting a light-weight approach to formal methods. In critical systems, such as medical systems, it is often easy to enhance the code with tracing information. ParTraP is a language that allows to express properties over traces of parametric events. It is designed to ease the understanding and writing of properties by software engineers without background in formal methods. In the tool demonstration video, we present the language and its toolset : evaluator, compiler, syntax directed editor.

Partrap reference documents

The ParTraP language syntax and semantics are described in " MODMED WP1/D2 and WP1/D3: Complete Definition of a Domain Specific Specification Language ". Other documents from the MODMED project are available at http://modmed.minmaxmedical.com/deliverables.

Toolset download and configuration

  1. We recommend to use Eclipse Oxygen or later with framework XText installed from : "https://www.eclipse.org/Xtext/" (Choose "Download" then "Download Eclipse" then under "Download Packages", and finally " Eclipse IDE for Java and DSL Developers ". Unzip and click on "eclipse.exe").
  2. You can also choose to install Eclipse DSL from the starting menu when installing Eclipse

  3. Download ParTrap Toolset as a site in the "install New software" (Eclipse Help menu) from this link "http://vasco.imag.fr/tools/partrap/toolset" (version corresponding to the video) or from "http://vasco.imag.fr/tools/partrap/toolset2.0" for more recent versions.


Getting started

Create a ParTraP project

Once you have installed the ParTraP plugin, you can create your first ParTraP project.

You should choose "New" from file menu then "Other" then "Partrap project". Enter a project name and click finish. A window asking to convert the project to an XText is opened you should validate by "OK". A project is created with all necessary materials for execution : jars and packages. An editor for ParTraP properties is opened. Now you can edit properties.

Use case examples

Sample trace files

Before executing any property you should have a json trace file.

You can download two examples of traces anywhere on your machine from http://vasco.imag.fr/tools/partrap/traces where you have one short trace "test_trace.json" and one long trace "long_trace.json".

Traces should conform to the following constraints in order to be exploited with the ParTraP language:

Simple ParTraP properties

Here is some starting properties examples that you can edit and test on the tool:

When saving, properties are compiled and you can execute them from "src-gen" package. You can also use the ParTraP Evaluator by right click on the editor window and choosing "Interprete Properties".

Selecting a trace file

To change the trace file you can right click on the ParTraP file from the project explorer window and choose "Update Trace File".

ParTraP Toolset with Python

To use Python expressions in the ParTraP toolset editor you should have a configured and working Jep with python. The eclipse ParTraP plugin is configured to work

Jep Installation Guide (under windows)

Jep can be found at the following address : https://github.com/ninia/jep/wiki/Getting-Started.

To install a working Jep Version with Eclipse you should follow the steps below:

Now that Jep is installed, you should exit and restart your eclipse environment (simply restarting is not sufficient). Then you should change the project properties by selecting "Python" in the "Partrap" option and then checking the button "enable Python support".

Some examples with python

Now you can use python expressions in the properties. Here are some examples:

Acknowledgements

This project is partly funded by the ANR MODMED project (ANR-15-CE25-0010).