Autor:
Lucio, Paqui

Foto de perfil
E-mails conocidos
paqui.lucio@ehu.es
paqui.lucio@ehu.eus
Fecha de nacimiento
Proyectos de investigación
Unidades organizativas
Puesto de trabajo
Apellidos
Lucio
Nombre de pila
Paqui
Nombre
Nombres alternativos
Afiliaciones conocidas
University of the Basque Country, Spain
Universidad del País Vasco, Spain
University of the Basque Country (UPV/EHU), Spain
The University of the Basque Country (UPV/EHU)
Universidad del País Vasco
Páginas web conocidas
Página completa del ítem
Notificar un error en este autor

Filtros

2016 - 201932020 - 20211
Restablecer filtros

Ajustes

Resultados de la búsqueda

Mostrando 1 - 4 de 4
  • Miniatura
    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.
  • Miniatura
    Artículo
    A Tutorial on Using Dafny to Construct Verified Software
    Lucio, Paqui. Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016), 2016-09-02.
    This paper is a tutorial for newcomers to the field of automated verification tools, though we assume the reader to be relatively familiar with Hoare-style verification. In this paper, besides introducing the most basic features of the language and verifier Dafny, we place special emphasis on how to use Dafny as an assistant in the development of verified programs. Our main aim is to encourage the software engineering community to make the move towards using formal verification tools.
  • Miniatura
    Artículo
    Context-based Model Checking using SMT-solvers
    Abuin, Alex; Díaz de Cerio, Unai; Hermo, Montserrat; Lucio, Paqui. Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018), 2018-09-17.
    In this paper we propose a new idea for the implementation of symbolic model checking. Our pro- posal takes advantage of two technologies. First, SMT-solvers as efficient auxiliary tools to perform a large proportion of the computational task. Second, the context-based tableau that is especially well suited for providing certificates of proved properties, as well as counterexamples of disproved properties. We mainly introduce the algorithm to be implemented, along with illustrative examples.
  • Miniatura
    Artículo
    Towards the Automatic Verification of QCSP tractability results
    Abuin, Alex; Chen, Hubie; Hermo, Montserrat; Lucio, Paqui. Actas de las XVII Jornadas de Programación y Lenguajes (PROLE 2017), 2017-07-19.
    We deal with the quantied constraint satisfaction problem (QCSP) which consists in deciding, given an structure and a rst-order sentence built from atoms, with conjunction and quantication, whether or not the sentence is true on the structure. We study a known proof system which has been used to derive QCSP tractability results. Our contribution is to formalize this proof system into an automatically veried theory, so that it can be used (in a near future) as a basis for automatically verify tractability results.