Formal Methods for Hard-Real Time Testing

Jan Peleska


We outline several problems and possible solutions for automated test data generation, test execution and test evaluation in the field of embedded hard real-time systems with both discrete and time-continuous (i.e. analog) interfaces. Test scripts are written as formal specifications which are - in pre-compiled internal representations - executable in real-time. We discuss the suitability of process algebras (Timed CSP) versus Hybrid Automata formalisms for these tasks. Automated test generation is based on standard solutions well known from process algebras, graph theory, logic and model checking. However, the necessary distinctions between input to the System Under Test (these parameters may be manipulated by the testing environment) and outputs (these parameters are checked against the specification) and the incorporation of real-time constraints require considerable extensions of the known theories.
Thursday 27th May 2004, 14:00
Robert Recorde Room
Department of Computer Science