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

Application domain/field

• Safety verification
• Real-time systems
• Component-based systems
• Compositional verification
• Invariant generation

Expected input

• Real-time BIP program
• Optional: Safety property

Format:

• Program: RT-BIP source file
• Safety property: Yices syntax. If this property is not provided then the tool will default to check deadlock-freedom.

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\wedge \neg \Psi$ is satisfiable. It will then report that (1) the property is satisfied, or (2) that it is not satisfied and a counterexample. Uses Yices