Analisis, validacion y depuracion de software
korrady27 de Marzo de 2014
2.910 Palabras (12 Páginas)258 Visitas
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. Por supuesto, existe una solucion: reemplazar
dichas libreras por otras alternativas en las que los metodos nativos
pueden ejecutarse de manera apropiada por Java PathFinder (lo que requiere
un considerable esfuerzo de implementacion, todava en desarrollo).
Resumiendo, Java PathFinder es una herramienta de veri cacion compleja,
con gurable y extendible. No se trata, por tanto, de una herramienta
sencilla y completamente automatica. A menudo requiere un cierto esfuerzo
de desarrollo para poder realizar tareas de veri cacion, validacion y depuraci
on de codigo Java. Como contrapartida, la experiencia en el proyecto
parece demostrar que hay errores que solo pueden encontrarse con Java
PathFinder. Cuando se trata de software crtico en el que un fallo no es una
opcion, Java PathFinder puede ser de mucha utilidad. No es sorprendente
que la herramienta haya sido desarrollada originalmente por el personal de
la NASA.
2.2. Testing vs model checking
Aunque una de las aplicaciones que vamos a ver de Java PathFinder es
la generacion automatica de casos de prueba basada en ejecucion simbolica,
en realidad Java PathFinder tambien puede, entre otras cosas, veri car
propiedades mediante model checking.
Las diferentes tecnicas de testing di eren en como se eligen los casos
de prueba, o en que informacion manejan (caja blanca, negra o gris) para
de nir y comprobar el buen comportamiento del sistema. El exito de su
aplicacion (es decir, encontrar o no los errores del sistema) dependen en
4
gran medida de esas elecciones de los casos de prueba o intuiciones de las
personas que realizan el testing. Si es un buen tester, encontrara el error, si
no lo es, entonces lo encontrara el usuario mas adelante.
Model checking es un metodo formal, lo que signi ca que no depende de
intuiciones o elecciones. En teora, si existe una violacion de la especi caci
on dada, la encontrara. Intuitivamente, model checking explora de forma
exhaustiva todas las posibles ejecuciones del sistema.
Con los programas concurrentes tenemos la di cultad extra de que no
sabemos cuando el sistema operativo va a dar el control a un thread o a
otro, por lo que deberamos ser capaces de probar el programa con distintos
schedulings, algo que no podemos controlar con casos de prueba. La
infraestructura de Java PathFinder le permite comprobar todos los posibles
schedulings para hacer model checking.
En ralidad, \todos los posibles casos" puede ser un numero demasiado
grande para los recursos y tiempo disponibles. Para solucionarlo, se puede
optimizar de forma automatica el model checker, se puede abstraer el sistema,
...