Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.
Publication
Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.
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.