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
- 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 :
- First dowload the RTD-Finder tool-set
- Extract the package.
- 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]
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.
rtdfinder -f benchmarkGear -r benchmarkGear -out Gear/Testgear.ys -p gearProp.ys
- 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
- Compositional Invariant Generation for Timed Systems, In TACAS’14 conference.
- Compositional Verification of Parameterised Timed Systems , In NFM’15 Conference, (to appear).
This tool is developed and maintained by Souha Ben Rayana.
For any question, please send an email to souha.benrayana imag.fr