Testing

URI permanente para esta colección:

https://hdl.handle.net/11705/PROLE/2021/TESTING
Artículos en la categoría Testing publicados en las Actas de las XX Jornadas de Programación y Lenguajes (PROLE 2021).
Notificar un error en esta colección

Examinar

Envíos recientes

Mostrando 1 - 3 de 3
  • 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
    Resumen
    Gaining Trust by Tracing Security Protocols
    Fredlund, Lars-Ake; Benac Earle, Clara; Arts, Thomas; Svensson, Hans. Actas de las XX Jornadas de Programación y Lenguajes (PROLE 2021), 2021-09-22.
    In this article we test an Erlang implementation of the Noise Protocol Framework, using a novel form of white-box testing. We extend interoperability testing of an Erlang enoise imple- mentation against an implementation of Noise in C. Testing typically performs a noise protocol handshake between the two implementations. If successful, then both implementa- tions are somehow compatible. But this does, for example, not detect whether we reuse keys that have to be newly gen- erated. Therefore we extend such operability testing: During the handshake the Erlang noise implementation is traced. The resulting protocol trace is refactored, obtaining as the end result a symbolic description (a functional term) of how key protocol values are constructed using cryptographic op- erations and keys. Therafter, this symbolic term is compared, using term rewriting, with a symbolic term representing the ideal symbolic execution of the tested noise protocol hand- shake (i.e., the “semantics” of the handshake). The semantic symbolic term is obtained by executing a symbolic imple- mentation of the noise protocol that we have developed.
  • Miniatura
    Artículo
    An application of KLEE to aerospace industrial software
    García, Juan Francisco; Jurjo, Daniel; Macías, Fernando; Morales, Jose F.; Gorla, Alessandra. Actas de las XX Jornadas de Programación y Lenguajes (PROLE 2021), 2021-09-22.
    This work reports the initial experience of the authors on the application of KLEE to industrial aerospace software. The software consists of C mission code for the Attitude and Orbital Control System (AOCS) subsystem, together with the Simulink models from which it was automatically generated. We detail the characteristics of the software we analyzed, the workflow we created to apply KLEE in the context of Model-Driven Development, and the results and challenges we found.