Description

The Optimization of Path ReAl-TimE Logic Tool (OPRATEL v1.0) is implemented in Java.

The class files can be downloaded freely from here (Copyright of its respective owners).

All tests have been conducted on a Pentium4 PC 1600Mhz, 512RAM, running on Windows XP and using Java SDK1.4.2_03.

Sample 1 - Railroad

Description of case study

“When the train approaches the sensor, a signal will initiate the lowering of the gate”, and “Gate is moved to the down position within 30s from being detected by the sensor”, and “The gate needs at least 15s to lower itself to the down position”.

The goal of this real-time system is described by the following safety assertions (denoted as SA):

“If the train needs at least 45s to travel from the sensor to the railroad crossing”, and “the train crossing is completed within 60s from being detected by the sensor”, then “we are assured that at the start of the train crossing, the gate has moved down and that the train leaves the railroad crossing within 45s from the time the gate has completed moving down”.

Problem specification:

In terms of RTL:

Conjunctive Normal Form (after skolemizing):

Constraints graph:

Specification file

Output file

Log file

Sample 2 - Reactor

This second case study is taken from [Jahanian, Mok, 1987]. It describes a system used to monitor and control a reactor. Please refer to the above mentioned paper for specification details.

For this sample we have also considered four situations, where we have intentionally "missed" one, two, three or four constraints. Following the same idea described above, we have considered the Jahanian-Mok specification as the "old" specification (see here our input file) and we have added and removed some constraints. Just for testing purposes, we have added up to four new, meaningless, nodes in the graph (new1 to new4).

Output file

Log file

Sample 3 - X38 avionics

This sample case is taken from [Rice, Cheng, 1999]. Please refer to this paper for complete specification of the sistem. The X-38 is an autonomous spacecraft designed and built by NASA as a prototype of the International Space Station Crew Return Vehicle.

For this sample we have also considered four situations, where we have intentionally "missed" one, two, three or four constraints. Following the same idea described above, we have considered the given specification as the "old" specification (see here our input file) and we have added and removed some constraints. Just for testing purposes, we have added up to four new, meaningless, nodes in the graph (new1 to new4).

Output file

Log file