The temporal rover and the ATG rover

Abstract

The Temporal Rover is a specification based verification tool for applications written in C, C++, Java, Verilog and VHDL. The tool combines formal specification, using Linear-Time Temporal Logic (LTL) and Metric Temporal Logic (MTL), with conventional simulation/execution based testing. The Temporal Rover is tailored for the verification of complex protocols and reactive systems where behavior is time dependent. The Temporal Rover generates executable code from LTL and MTL assertions written as comments in the source code. This executable source code is compiled and linked as part of the application under test. During application execution the generated code validates the executing program against the formal temporal specification requirements. Using MTL, real time and relative time constraints can be validated. A special code generator supports validation of such constraints in the field, on an embedded target.