Artículo:
Using Model Checking in Requirement-based Test Generation for Reactive Systems

Fecha

2021-09-22

Editor

Sistedes

Publicado en

Actas de las XX Jornadas de Programación y Lenguajes (PROLE 2021)

Licencia Creative Commons

Resumen

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.

Descripción

Acerca de Hermo, Montserrat

Palabras clave

Model Checking, Reactive Systems, Test Generation
Página completa del ítem
Notificar un error en este artículo
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX