Búsqueda avanzada

Using Model Checking in Requirement-based Test Generation for Reactive Systems


In this article we propose an automatic test generation technique for evaluating the implementation of a reactive system with respect to the set of requirements from which it has been developed. We consider reactive systems that interact with its environment via variables whose values (at each instant) depends on events or sensors. Our test cases are graphs that represent a collection of executions (or traces) of the system that captures all possible behaviours of the environment. Our proposal is a technique to automatically construct these graphs exploding the ability of model checkers to generate counter-examples for temporal properties that are not satisfied by a system model. Further work includes to implement a prototype for experimenting the technique on a test suite of industrial requirements, and also to design and implement some techniques to gain scalability.

Palabras Clave:

Model checking - Reactive Systems - Test Generation





Este artículo tiene una licencia de uso CreativeCommons - Reconocimiento (by)

Descarga el artículo haciendo click aquí.

Ver la referencia en formato Bibtex