Oca, Josu

Foto de perfil

E-mails conocidos

Fecha de nacimiento

Proyectos de investigación

Unidades organizativas

Puesto de trabajo



Nombre de pila



Nombres alternativos

Afiliaciones conocidas

University of the Basque Country, Spain

Páginas web conocidas

Página completa del ítem
Notificar un error en este autor

Resultados de la búsqueda

Mostrando 1 - 2 de 2
  • Artículo
    Using Model Checking in Requirement-based Test Generation for Reactive Systems
    Hermo, Montserrat; Lucio, Paqui; Oca, Josu. Actas de las XX Jornadas de Programación y Lenguajes (PROLE 2021), 2021-09-22.
    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.
  • Artículo
    Towards an Efficient Implementation of Tableaux for Reactive Safety Specifications
    Alonso, Ander; Hermo, Montserrat; Oca, Josu. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.
    In this article, we take the first steps to implement a tableau method for deciding realizability of specifications expressed in a safety fragment of linear temporal logic. This tableau method also allows us to extract (i.e., synthesize) a correct system in the case the specification is realizable. In particular, we explain here how to efficiently implement a new normal form called terse normal form, which is crucial to the development of such tableau method.