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 de estados".

De entrada, Java PathFinder emplea una tecnica para evitar explorar

aquellos caminos que alcanzan un estado que es similar a otro estado

ya explorado.

Como hemos dicho, la principal utilidad de Java PathFinder consiste en localizar

errores en el programa a vericar. En principio, el tipo de errores depender

a de la conguracion, aunque Java PathFinder es capaz de encontrar un

cierto numero de errores sin necesidad de conguracion alguna: deadlocks y

3

excepciones no capturadas, por ejemplo. Se trata de propiedades no funcionales

que ninguna aplicacion debe violar. Sin embargo, Java PathFinder nos

permite tambien denir nuestras propias propiedades mediante los llamados

listeners, peque~nos plugins que nos permiten monitorizar todas las acciones

realizadas por jpf-core, tales como la ejecucion de instrucciones individuales,

la creacion de objetos, alcanzar un nuevo estado, etc. Un ejemplo de listener

es el detector de condiciones de carrera, es decir, situaciones en las que varios

procesos concurrentes pueden acceder a un mismo recurso compartido y, al

menos uno de ellos, va a modicarlo. Se trata de situaciones que pueden dar

lugar a errores dependiendo del orden de acceso.

Tambien resulta muy util en Java PathFinder la posibilidad de revisar el

historico de instrucciones ejecutadas {la traza de ejecucion{ hasta el mismo

punto del error, lo que puede resultar muy util para localizar el motivo del

mismo.

Por supuesto, la contrapartida a tantas facilidades en Java PathFinder es

que normalmente se requiere un esfuerzo importante de conguracion e, incluso,

de programacion. Otra complicacion adicional es que jpf-core no puede

emplear libreras de Java que usen codigo nativo. El motivo es basicamente

que Java PathFinder no sabra que hacer con llamadas al sistema para leer o

escribir en un chero, por ejemplo.

...