PV4 RTD-Findercan check deadlock-freedom and user-specified safety properties of RT-BIP models

Application domain/field

Expected input

Format:

Expected output

It will report whether the safety property is satisfied or not. If it is not satisfied, then it will also provide a counterexample.

Internals

It takes as input a RT-BIP model and a safety property to check for. Then it computes a global invariant. The idea is that this global invariant encodes the components of the system and the interactions relating them. This invariant is sometimes called the interaction invariant because of this. The invariant together with the safety property are then given to the Yices solver to check whether GI¬Ψ is satisfiable. It will then report that (1) the property is satisfied, or (2) that it is not satisfied and a counterexample. Uses Yices

Links

Project page: www-verimag.imag.fr/RTD-Finder

Related papers

RTD-Finder: A Tool for Compositional Verification of Real-Time Component-Based Systems (TACAS '16)

Last publication date

9 April 2016

Related tools

D-Finder: similar system for untimed systems.

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.