Welcome to TemPsy-Check

TemPsy-Check is a toolset to perform offline checking of TemPsy properties on system execution traces. The toolset has been developed by Wei Dou (http://people.svv.lu/dou), at the SVV lab (http://www.svv.lu) of the University of Luxembourg (http://wwwen.uni.lu). More information on TemPsy-Check is available in this technical report:

Wei Dou, Domenico Bianculli, and Lionel Briand. A model-based approach to trace checking of temporal properties with OCL. Technical Report TR-SnT-2014-5, SnT Centre - University of Luxembourg, September 2014. Available online at http://hdl.handle.net/10993/16112

TemPsy is a domain specific language based on OCL (Object Constraint Language, http://www.omg.org/spec/OCL) which allows users to express temporal properties using property specification patterns (http://patterns.projects.cis.ksu.edu). TemPsy is a redefined language of OCLR, which has been introduced in this paper:

Wei Dou, Domenico Bianculli, and Lionel Briand. OCLR: a more expressive, pattern-based temporal extension of OCL. In Proceedings of the 2014 European Conference on Modelling Foundations and Applications (ECMFA 2014), York, United Kingdom, volume 8569 of Lecture Notes in Computer Science, pages 51-66. Springer, July 2014. Available online at http://dx.doi.org/10.1007/978-3-319-09195-2_4

Requirements

• Mac OS X / Linux
• Xtext framework (http://xtext.org) 2.5.0+
• Java 1.6.0_65
• Eclipse OCL 4.1.0

Content of the distribution

The TemPsy-Check distribution contains two modules:

Checker (checker folder)

The offline trace checker is comprised of four parts: the TemPsy-Check main programs, the models, the DSLs, and the mapping from TemPsy to OCL.

• In the main folder, OfflineCheck.java is the main program for checking TemPsy properties. The other Java program ConstraintFactory.java is an auxiliary class for building OCL constraints and/or queries.
• The models folder contains three Ecore models: a trace model, an TemPsy meta model, and a check model. By using the three models, we generate the corresponding Java code and check the traces with our checker programs.
• the DSLs folder contains the Xtext definitions (Trace.xtext and Oclr.xtext) of the trace model and of the TemPsy meta model. It also contains the programs for building XMI instances of the two models.
• The oclr2ocl folder contains the definition of the translation that maps TemPsy constraints into OCL constraints on the trace model.

Evaluation

This module contains the artifacts used to perform the evaluation described in the aforementioned technical report: the TemPsy properties and the trace generators used to generate the traces.

• Properties

  We provide 38 TemPsy properties, both as DSL specifications (under the TemPsy-DSL-specifications folder) and as XMI instances (under the TemPsy-XMI-instances folder) conforming to the TemPsy meta model. These XMI instances are generated from the DSL specifications by using the program: "/checker/DSLs/TemPsyInstanceFactory.java".

• Trace Generators

  Traces generator programs implement various generation strategies, depending on the type of property that one wants to check on the trace being generated. Generators are Python programs named after the type of property for which they generate traces; e.g., trace_generator_globally.py is the trace generator to generate the trace for the properties with the globally scope. A trace generator needs 4 parameters:

  1. scope (--scope/-s SCOPE);
  2. pattern (--pattern/-p PATTERN);
  3. property id (--id/-i ID);
  4. (maximum) trace length (--length/-l LENGTH). For instance: ./trace_generator_globally.py -s 'globally' -p 'always a' -i p1 -l 1000000 corresponds to generating traces with various trace lengths - 100K, 200K, ..., 1M (determined by the given maximum trace length) for the property with id p1 which has the scope globally and the pattern always a. We also provide the shell scripts used to generate the traces for the 38 properties contained in the releases.

• Traces

  For each property to check, we provide several traces both in CSV and XMI formats. The XMI traces were generated by the trace generators introduced below, and the CSV traces were automatically transformed from the XMI ones. To keep the size of the repository small, we provide the traces in separate releases (https://github.com/weidou/TemPsy-Check/releases/tag/v1.0-csv and https://github.com/weidou/TemPsy-Check/releases/tag/v1.0-xmi).

  Usage

  Please read the usage guide on the Wiki.