The TL Compiler

This paper describes a method of compiling specification properties into automata or test oracles which allow testing of any proposed implementation. It also shows how to interpret the automata's status during testing. The method addresses verification of reactive systems, including distributed object oriented applications. TL (Temporal Logic) has been chosen as specification language. The basic future temporal operators and logical operators are supported. The automaton generated from a specification property (also called behavioural constraint) does not depend on the semantics of input events, such that the TL compiler can be used as a module in any verification system. The verification tool could be using a system description language to express proposed implementations or run-time execution traces of the actual implementation.