zbMATH — the first resource for mathematics

The Temporal Rover and the ATG Rover. (English) Zbl 0976.68571
Havelund, Klaus (ed.) et al., SPIN model checking and software verification. 7th international SPIN workshop, Stanford, CA, USA, August 30 - September 1, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1885, 323-330 (2000).
Summary: 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.
For the entire collection see [Zbl 0947.00033].

68U99 Computing methodologies and applications
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)