Analisis, validacion y depuracion de software

Analisis, validacion y depuracion de

software

Practica 3

Herramientas de Testing: Java Pathnder

German Vidal

Alicia Villanueva

Curso 2013/2014

Indice

1. Introduccion 2

1.1. Objetivo de la practica . . . . . . . . . . . . . . . . . . . . . . 2

1.2. Material adicional . . . . . . . . . . . . . . . . . . . . . . . . 2

2. Java PathFinder 2

2.1. Introduccion . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

2.2. Testing vs model checking . . . . . . . . . . . . . . . . . . . . 4

2.3. Symbolic Java PathFinder . . . . . . . . . . . . . . . . . . . . 5

3. Instalacion 6

4. Ejercicios 9

4.1. Programa Random . . . . . . . . . . . . . . . . . . . . . . . . 9

4.2. Programa Race . . . . . . . . . . . . . . . . . . . . . . . . . . 11

1. Introduccion

En esta tercera practica, vamos a introducir una herramienta para realizar

pruebas del software (testing) basada en la ejecucion simbolica.

1.1. Objetivo de la practica

El objetivo de la practica consiste en que los alumnos conozcan los fundamentos

de la herramienta Java PathFinder y se familiaricen con la salida producida

por la misma. En particular, veremos como se realiza la instalacion

de la herramienta (por lo que al nalizar la practica, el alumno dispondra de

la instalacion de Java PathFinder en su directorio personal) y estudiaremos

algunos ejemplos de ejecucion.

Los alumnos deberan enviar en el plazo indicado en la tarea de

PoliformaT los cheros asociados a los ejercicios 1 a 4.

1.2. Material adicional

A continuacion, presentamos una lista de material bibliograco que puede

servir de apoyo:

Wiki ocial de la herramienta:

http://babelfish.arc.nasa.gov/trac/jpf

Wiki ocial del proyecto de ejecucion simbolica:

http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc

2. Java PathFinder

Java PathFinder es un entorno de ejecucion de bytecodes {el codigo intermedio

generado por el compilador{ de Java que dispone de muchas opciones

de conguracion. La principal aplicacion de Java PathFinder es la vericacion

y validacion (mediante generacion de casos de prueba) de programas Java.

El sistema ha sido desarrollado por la NASA (Ames Research Center) y se

trata de un proyecto de codigo abierto y gratuito desde 2005.

2.1. Introduccion

Java PathFinder esta desarrollado de forma modular, de manera que pueda

extenderse facilmente con nuevos componentes. Antes de pasar a trabajar

con ejecucion simbolica, conviene entender la estructura de la herramienta.

Por ello, a continuacion vamos a centrarnos en el modulo principal: jpf-core.

jpf-core es una maquina virtual para bytecodes de Java, lo que signica

que es un programa que nos permite ejecutar programas Java (compilados),

2

Figura 1: Esquema basico de jpf-core

de forma similar a la JVM que incorporan, por ejemplo, los navegadores.

Java PathFinder se usa para encontrar errores en los programas, por lo que

en general habra que indicarle de algun modo el tipo de propiedad que

queremos comprobar. Como resultado, jpf-core genera un informe con informaci

on acerca de si las propiedades se cumplen o no, as como los artefactos

de vericacion oportunos (por ejemplo, casos de prueba). Algunas de las

particularidades de jpf-core son las siguientes:

Aunque se trata de una maquina virtual como la JVM de los navegadores,

esta implementada en el propio lenguaje Java (por lo que

normalmente sera algo mas lenta).

El conjunto de instrucciones de la maquina virtual esta representado

mediante un conjunto de clases que puede reemplazarse o extenderse.

El conjunto de instrucciones por defecto usa execution choices (elecciones

de ejecucion) para determinar como proceder cuando se alcanza

un punto de ejecucion con varias opciones. Normalmente, Java Path-

Finder explorara sistematicamente todas posibilidades cada vez que

aparezcan valores aleatorios, diferentes alternativas en las estrategias

de ejecucion concurrente de procesos, etc.

Por supuesto, explorar \todos los caminos posibles" implica a menudo

un problema de escalabilidad, ya que el espacio de posibles ejecuciones

puede crecer exponencialmente. Esto es lo que se conoce en la literatura

sobre el tema como \el problema de la explosion

...