Home > Verimag > Tools

RTD-Finder

  • Software distribution and licensing: Public binary distribution
  • Software maturity: Basic usage works, terse documentation.
  • Software Maintenance and Evolution: Basic maintenance to keep the software alive, no future plans
A COMPOSITIONAL VERIFICATION TOOL FOR Real-time BIP MODELS

 Method

The RTD-Finder tool implements a compositional method for the verification of component-based real-time systems. It aims to avoid state-space exploration techniques which suffer in general from state-space explosion for systems with large number of components. The basic idea is to infer properties of a system from the properties of its components and the interactions relating them. In order to track time synchronization between the different components in a compositional manner, we use additional history clocks, which do not influence the behavior of the system, and which are used during the verification process . To each action (resp. interaction), we associate a history clock which is reset whenever the related action (resp. interaction) occurs. The actions history clocks are considered during the computation of the local components invariants. This induces relations between the clocks of each component and its history clocks. On the other hand, relations between the history clocks of different components are inferred from the interactions structure. They are formulated in an additional invariant as the history clocks constraints. By transitivity, relations between the inner clocks of different components are induced. The tool computes the interaction invariant, constraining the global locations of the system, as in the DFinder tool which was designed for untimed systems. All the above invariants are gathered in the global invariant, offering an over-approximation of the reachable states set of the system.

The tool takes as input a RT-BIP model and a safety property to check for invariance. After computation of the global invariant, RTD-Finder exports it, together with the safety property, to the YICES sat-solver. If no counter-example is generated, the property is valid.

 How To Install and Run RTD-Finder

Requirements:

  • Linux.
  • Java 1.6

We note that RTD-Finder takes as input a RT-BIP system modeled following the new BIP language. To install the RTD-Finder tool, please follow these steps :

  • The main directory contains :
    • lib/ directory that contains libraries used by the tool,
    • bin/ directory that contains the tool binaries,
    • examples/ directory that contains RT-BIP examples,
    • safetyProp/ directory that contains the properties to ckeck,
    • output/ directory that contains the generated Yices output files,
    • setup.sh script to set up the environment, and
    • README file that describes the tool in detail.

To use the tool on command line, you have to source the setup.sh in order to add the binary files to you path:

$ source setup.sh
  • Go to the RTD-Finder main directory and run the RTD-Finder tool to verify your model using this command:

rtdfinder  -f [path-to-model]    -r [name-of-root-component]    -p [safety-property-file]    -out  [path-to-output-file.ys]

 Running Examples

In terminal, go to RTD-Finder folder. For each of the following examples, run the corresponding command:

Temperature Control System

rtdfinder    -f TC50 -r  TC50   -out TC/testTC50.ys -p TC50prop.ys

This command takes as input the model from the BIP file TC10.bip ( [examples] folder), the root component name (TC10), and the property file <TC10prop.ys> to check for invariance (under [safetyProp] subfolder). These running arguments correspond to the Temperature control system with 10 rods. RTD-Finder generates the invariant, exports it to the output file together with the provided safety property and executes Yices in order to check the existence of a counter-example. In the examples sub-folder, we provide BIP model files corresponding to different numbers of rods. We provide also the output yices files in output -> TC sub-folder.

Train Gate Controller System

rtdfinder    -f TGC50 -r  TGC50  -out TGC/testTGC50.ys -p TGC50prop.ys

The yices files for the TGC models that we have tested can be found under output ->TGC subfolder.

Gear Controller

rtdfinder -f benchmarkGear  -r benchmarkGear    -out Gear/Testgear.ys -p gearProp.ys

Implantable Pacemaker

  • Use of history clocks to express the safety property rtdfinder -f Pacemaker -r  Pacemaker  -out Pacemaker/testPacemaker.ys -p pacemakerProp.ys  
  • Use of a monitor component to model the safety property : rtdfinder -f PacemakerMonitor -r  PacemakerMonitor -out Pacemaker/testPacemakerMonitor.ys -p pacemakerPropMoni.ys  

A Timed Token Ring Protocol

rtdfinder -f  tokenRing5  -r  tokenRing5 -out TR/testTR5.ys -p tr5prop.ys  

 Related Papers

  • Compositional Verification of Parameterised Timed Systems , In NFM’15 Conference, (to appear).

 Contact

This tool is developed and maintained by Souha Ben Rayana.

For any question, please send an email to souha.benrayana@imag.fr


New publications