Navegación

Búsqueda

Búsqueda avanzada

Resultados de búsqueda para runtime monitoring

Testing Temporal Logic on Infinite Java Traces

This paper summarizes an approach for testing reactive and concurrent Java programs which combines model checking and runtime monitoring. We use a model checker for two purposes. On the one hand, it analyzes multiple program executions by generating test input parameters. On the other hand, it checks each program execution against a linear temporal logic (LTL) property. The paper presents two methods to abstract the Java states that allow efficient testing of LTL. One of this methods supports the detection of cycles to test LTL on potentially infinite Java execution traces. Runtime monitoring is used to generate the Java execution traces to be considered as input of the model checker. Our current implementation in the tool TJT uses Spin as the model checker and the Java Debug Interface (JDI) for runtime monitoring. TJT is presented as a plug-in for Eclipse and it has been successfully applied to complex public Java programs.

Autores: Damián Adalid / Alberto Salmerón / María del Mar Gallardo /  Damián Adalid, Alberto Salmerón, María del Mar Gallardo and Pedro Merino / 
Palabras Clave: Model checking - runtime monitoring - Testing

No encuentra los resultados que busca? Prueba nuestra Búsqueda avanzada