Subproject

S1

Categories

Systems of systems / blackbox tools, Model checker for hard & soft real-time systems

Overview

timemachine is a bounded model checker for incomplete networks of timed automata to prove unrealizability of an invariant. This tool supports multiple prevalent communication models, and allows the user to select several subautomata of the network as blackboxes. Furthermore, it can be specified how the unknown behavior of each blackbox output is modeled (abstraction technique based on fixed transitions or based on universal quantification). timemachine uses Yices and MathSAT as back-end SMT solvers. If a more precise modeling based on universal quantification is required, the resulting quantified SMT formulas are solved using either LIRA or LinAIGs. As input, timemachine accepts networks of timed automata given in the standard UPPAAL file format.

Publications

C. Miller, K. Gitina, C. Scholl, B. Becker. Bounded Model Checking of Incomplete Networks of Timed Automata. In Proc. of Microprocessor Test and Verification Workshop (MTV), 2010.

C. Miller, C. Scholl, and B. Becker. Verifying Incomplete Networks of Timed Automata. In Proc. of GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2011.

Benchmarks

Timed Blackbox BMC Suite

Download

Click here for the binary.

Manual

Just type ./tm-static on the command line to see how it can be used.

Status

Prototype