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 videos, we present the language and its toolset:
ParTraP-IDE (evaluator, compiler, syntax directed editor)
and ParTraP-EG (generator of trace examples and counter-examples).
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").
You can also choose to install Eclipse DSL from the starting menu when
Once you have installed the ParTraP-IDE 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
Use case examples
Sample trace files
Before executing any property, you should have a json trace file.
Traces should conform to the following constraints
in order to be exploited with the ParTraP language:
The top level element should be an array of json objects representing events.
Each event has a set of parameters.
Mandatory parameters are "id" (an identifier representing the event name)
and "time" (a number: an integer or a floating point representing the event time-stamp).
An event can have other parameters.
Simple ParTraP properties
Here is some starting properties examples that you can
edit and test on the tool:
VAlidTemp1: after first
CameraConnected, absence_of Temp t where t.v1<45;
ValidExit: EnterState ee
followed_by ExitState xx where ee.state==xx.state;
each EnterState ee where
ee.state=='mainCasp.TrackingConnection.TrackersVisibCheck', given last
SearchTrackers st, forall type in st.types, occurrence_of
TrackerDetected td where td.ty ==type;
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 plugins is configured to work
under windows 10
with python 3.6
using jep 3.7.1 (you can build it with "pip install jep==3.7.1")
(jep is built using "Visual Studio Building tools 2015")
To install a working Jep Version with Eclipse you should follow the steps below:
Installing Python: from "this link".We recommend version 3.6 since it corresponds to the jep in the plugin.
The Python configuration (32bits or 64 bits) should be the same as Java.
It might be useful to declare the environment variable "python" with the path to the executable command.
Installing pip: pip is already installed in Python 2 >=2.7.9 or Python 3 >=3.4. Otherwise, you can install it from "here".
Installing Numpy: it is a Python package, mandatory for Jep to work. You can download the last release from this link "here".
Installing Jep: now that all modules are installed, Jep package should be downloaded from this "link".
Open a command prompt as admin with visual C++ environment variables (in the windows menu, choose Visual C++2015, locate a command prompt corresponding to your machine (32 or 64 bits), click right on this menu entry,
and choose "More > Run as administrator").
In the command prompt you execute either "pip install jep" or "python setup.py install".
Jep is installed but you have to configure it to be accessible by Eclipse.
You should either add to the Windows PATH the directory "C:\Program Files\Python36\Lib\site-packages\jep",
or to declare the environment variable "LD_LIBRARY_PATH" with the path to the "jep.dll" situated under python "\Lib\site-packages\jep" (setting the LD_LIBRARY_PATH is mandatory if you work on the source code of the ParTraP plugin).
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
test_py1: occurrence_of 3
EnterState ee where $'load profile' in ee.state$;
test_py2: ExitState ee
preceded_by EnterState es where $fabs(es.time-ee.time)<10 and
test_py3: given last
SearchTrackers st, forall type in $['P','F','T','R']$, occurrence_of
TrackerDetected td where td.ty==type;
Generation of trace examples with ParTraP-EG
Once you have installed the ParTraP-IDE and ParTraP-EG plugins, you can first create ParTraP project
and ParTraP properties using ParTraP-IDE (see above).
To generate a trace example, you can right click on the ParTraP property from the project explorer window
and choose "ParTraP-EG/ Generate Trace Example".
An SMT2 file that specifies the property in SMT-LIB language is created in the folder "src-gen".
A JSON trace file that satisfies the property is created in the folder "trace-examples".
ParTraP-EG may return UNSAT if the property is unsatisfiable, or UNKNOWN when it cannot determine whether a property is satisfiable or not.
You can generate a trace counter-example from the negation of the property.
You can evaluate the satisfiable ParTraP property over the generated traces using ParTraP-IDE (see above).
This project is partly funded by the ANR MODMED project (ANR-15-CE25-0010).