Verificación y Validación de Software con Destiny: Un enfoque paralelo a la
prueba automática de teoremas
por Josiah Dykstra
traducido por Sergio Roa Ovalle
Resumen
Este artículo presenta una introducción a la prueba de teoremas asistida por
computador y un nuevo enfoque usando procesamiento paralelo para incrementar la
potencia y velocidad de esta computación. Los probadores automáticos de
teoremas, junto con la interpretación humana, han sido vistos como herramientas
poderosas en la verificación y validación de software computacional.
Destiny es una nueva herramienta que provee un análisis aún más grande y
más poderoso facilitando un mayor acoplamiento entre los programas de software y
sus especificaciones.
Introducción
El desarrollo de software computacional es un proceso tedioso. Contrario al
hardware, el software puede ser actualizado y transformado fácilmente, y por
tanto, frecuentemente. Por consiguiente, diversas ideologías de actualización se
han desarrollado incluyendo las de "construye primero, corrige después", "si
corre, envíalo" y "siempre existirán errores en el programa (bugs), así que sólo
corrige los peores". Adicionalmente, el proceso de desarrollo del software tiene
una tendencia a producir un producto incrementalmente complejo y progresivamente
defectuoso. Por esta razón, es casi que imposible alcanzar la confiabilidad; aún
con un requerimiento de diseño primario. En aplicaciones de alta seguridad, esto
presenta una grave situación. Un programa no solamente debe estar libre de
errores, sino que es igualmente importante que el rendimiento del programa final
no sea mayor o menor a lo proyectado originalmente. Escribir un programa que se
ejecute como se planeó no es una tarea simple. Por lo tanto, el proceso de
software incluye verificación y validación, donde la validación es el proceso de
responder la pregunta, "¿Construimos el producto correcto?" y la verificación
responde a la pregunta "¿Construimos el producto correctamente?"[5]. G. J. Myers dijo, "El test es el proceso de ejecutar
programas con la intención de encontrar errores." Pero, de acuerdo a E. W.
Dijkstra, "El test puede mostrar la presencia de errores (bugs), pero nunca su
ausencia"[6]. Se han dedicado muchos años de investigación
para un último fin: probar que los errores no existen.
Los métodos formales son la aplicación de las técnicas matemáticas
para la especificación, el análisis, el diseño y la implementación de software y
hardware computacional complejo. La lógica computacional es una lógica
matemática mecanizada para chequear pruebas por computación. Combinando estas
dos, uno debería ser capaz de atacar el problema de la validación y verificación
de software y hardware. En teoría, uno puede demostrar matemáticamente que un
programa se ciñe a una especificación. Si, por ejemplo, un programador
implementa un algoritmo, un analista puede traducir el código fuente a una forma
funcional y usar un demostrador de teoremas para probar formalmente que el
código va a satisfacer los requerimientos dados. Esto también quiere decir que
podemos identificar si el algoritmo fallará, producirá errores, o sucumbirá ante
datos de entrada inesperados o formateados inapropiadamente. A pesar de esto,
uno no puede garantizar una inmunidad a cualquier mal funcionamiento (detección
de interbloqueos, por ejemplo); sin embargo, bajo el supuesto que estos
requerimientos son cumplidos, se garantiza matemáticamente que el programa
resultante esté libre de errores en su ejecución, y exactamente como se desea.
La Prueba de Teoremas en la Actualidad
Muchos trabajos previos relacionados con la prueba o demostración de teoremas y
el desarrollo de software utilizando las técnicas de prueba de teoremas
provenían de Robert S. Boyer y J. Strother Moore en la Universidad de Texas en
Austin. A Computational Logic, de Boyer y Moore, publicado en 1979 y
continuado en una Segunda Edición en 1998, es un manual que incluye una cartilla
de lógica como un lenguaje de programación funcional y una guía de referencia
detallada a los sistemas asociados de prueba mecánica de teoremas [1]. El sistema que ellos describen, y que distribuyen
ampliamente, es llamado Nqthm. El programa está basado en Common Lisp, y se han
producido varias versiones. Desde principios de los años 1990s, Matt Kaufmann y
Moore han estado trabajando en un nuevo probador de teoremas, llamado "Una
Lógica Computacional para Common Lisp Aplicativo", o ACL2 (por sus iniciales en
inglés - A Computational Logic for Applicative Common Lisp)[7].
Nqthm ha sido ampliamente aceptado y usado como una herramienta poderosa,
probando cosas como un pequeño kernel (núcleo) de sistema operativo multitarea
cumpliendo con su especificación [1], la invariabilidad
del algoritmo de encriptamiento de llave pública RSA [3],
y diferentes protocolos de comunicaciones [4]. ACL2 está
siendo adoptado lentamente por instituciones académicas y centros de
investigación en todo el mundo.
Destiny es una plataforma aplicativa diseñada con la retrospectiva en mente
de los probadores de teoremas previos. Destiny provee una interfaz gráfica y
favorece la interacción con los resultados producidos. Varios niveles de
diagramas de flujo de control son generados suministrando al analista
niveles más profundos de información, si es necesario. Adicionalmente, está
diseñado para el procesamiento paralelo escalable. Este método "divide y
vencerás" significa que cuando los problemas se vuelven más y más complejos,
se puede incrementar poder computacional adicional para contrarrestar esto.
Esencialmente, el dominio de un problema grande es fraccionado en pequeños
conjuntos de problemas a ser resueltos individualmente, y al combinarse se
produce la respuesta final. Finalmente, la versión actual de Destiny acepta el
código Java como entrada. Mientras que Destiny convierte el programa a la forma
funcional, Nqthm y ACL2 requieren que la entrada original sea construida en
Lisp.
Una Plataforma para Modelamiento Java
Java fue escogido por diversas razones. El lenguaje Java fue diseñado por Sun
Mycrosystems para que corriera sobre una especificación detallada de una máquina
virtual, que ha sido portada a varias arquitecturas de hardware. La portabilidad
y la independencia de implementación de la Máquina Virtual Java (JVM por sus
iniciales en inglés - Java Virtual Machine) permite que Destiny funcione sobre
un conjunto más grande de problemas. Cualquier programa Java puede ser modelado
sin pensar en cómo ha sido implementada la JVM; para el programador, el conjunto
de instrucciones de la JVM es consistentemente el mismo. En la JVM, el código de
ejecución es organizado en una pila de "marcos" (frames). El marco de un método
de ejecución mantiene las variables locales y una pila de operandos, que imitan
los registros de una CPU en hardware.
Las clases Java son cargadas dinámicamente cuando un programa las necesita.
La primera vez que una clase es accedida, el ambiente en tiempo de ejecución
carga la clase y realiza las operaciones necesarias para usarla. Como Destiny
nunca ejecuta el programa introducido, un paso inicial es requerido en el
código fuente, ya que se registran todas las llamadas de librerías y las
referencias externas para estar seguros de que cualquier código Java que está
cargado será ejecutado. Usando esta característica, podemos construir un grafo
dirigido demostrando todas las rutas posibles de la ejecución del programa.
Cada vértice del grafo representa un código de operación, y las aristas
describen la transición entre instrucciones. La invocación y retorno de control
dado por llamadas a métodos con la ayuda de Java dan al programa una forma
distinta y bloques discretos. Este conocimiento puede ser usado para construir
un grafo de métodos de más alto nivel, con cada vértice representando un método
completo y las aristas mostrando llamadas y retornos. El análisis y la
evaluación pueden ser hechos ahora sobre los métodos o segmentos de código
aislados. Cada vértice está asociado con una transición de estado, una expresión
formal describiendo cómo la ejecución de ésta alterará la máquina virtual. Cada
arista está asociada con un predicado, un requerimiento condicional para seguir
la ruta dada.
Por ejemplo, una sentencia if-then-else determina qué bifurcación seguir basados
en un condicional, como se ve en las Figuras 1 y 2. Un recorrido a través del
proceso actual de Destiny demuestra la progresión desde el código objeto Java al
código byte, hasta las interfaces gráficas de método y código byte. Este proceso
es ilustrado en las Figuras 3-6. La interacción es alcanzada permitiendo al
analista hacer click sobre cualquier vértice para mayor información o para
construir el grafo del siguiente nivel de detalle.
Boolean verified;
if(x==5){
verified = true;
}
else{
verified = false;
}
|
Figura 1: Sentencia If-Then-Else mostrando bifurcación del código.
Figura 2: Diagrama de transición de estados ilustrando
el código de la Figura 1.
import java.io.*;
public class SimpleProgram {
public static void main(String args[]){
String x = args[0];
int n = Integer.parseInt(x);
int sum = 0;
boolean verified = false;
for (int i=1; i<=n; ++i){
sum = sum+i;
}
if (sum = n * (n+1)/2){
verified = true;
}
}
}
|
Figura 3: Programa de ejemplo que verifica la suma de enteros de 1 hasta
n.
0 aload_0 // String x = args[0]
1 iconst_0
2 aaload
3 astore_1 // int n = Integer.parseInt(x)
4 aload_1
5 invokestatic #2
8 istore_2
9 iconst_0 // int sum = 0
10 istore_3
11 iconst_0 // boolean verified = false
12 istore 4
14 iconst_1 // for (int i=1; i<=n; ++i){
15 istore 5
17 goto 28
|
Figura 4: Código byte Java compilado a partir del código fuente Java de la
Figura 3. 
Figura 5: Grafo Destiny de Método (grafo de alto nivel) mostrando un
método definido (main) y el inicializador JVM construido.
Figura 6: Grafo Destiny de Código Byte (grafo de bajo nivel)
completo (izquierda) y ampliado (derecha).
Prueba de Teoremas en paralelo
El uso de Destiny de las ideas tras un cluster Beowulf lo hace
excepcionalmente poderoso. Un cluster Beowulf es una colección de
computadores, de los que se encuentran habitualmente en el mercado, corriendo en
paralelo mediante una red privada, que rivaliza con el poder de los
supercomputadores a un costo sustancialmente reducido. La implementación Destiny
del cluster involucra dos dominios autónomos de red, el anillo de datos y
la estrella de balance de carga. El hardware que lo soporta consiste en un
maestro en el centro de una estrella de esclavos, conectados para formar un
anillo (Figura 7).
Figura 7:
Arquitectura Destiny mostrando estrella de balance y anillo de
datos.
Estrella de Balance de Carga
Cuando Destiny corre, genera eventos, los cuales son módulos, que consisten de
estados y código, que son ejecutables y persistentes. Solamente aquellos eventos
que son capaces de importar y exportar pueden ser candidatos para balance de
carga a través de los esclavos. El maestro modera el servicio de balance de
carga. Cuando Destiny empieza inicialmente su ejecución, los eventos que
necesitan ser procesados son pasados a un único esclavo. Cuando la carga se
incrementa y el esclavo se satura, los eventos son reenviados a otros esclavos
con el fin de reducir la carga. El maestro mantiene la única cola de eventos. La
implementación actual ha sido realizada con un maestro y veintitrés esclavos
usando un conmutador (switch) de 24 puertos de alta velocidad y
TCP/IP.
Anillo de Datos
El anillo de datos es para uso exclusivo de los esclavos. Dos aplicaciones
corren sobre cada esclavo: un controlador y un procesador de trabajo. El
controlador actúa como un enlace entre el procesador de trabajo esclavo y el
maestro, dejando al procesador de trabajo que se concentre exclusivamente en el
procesamiento de datos. Con esta configuración se pretende apoyar a los esclavos
con la capacidad de multiprocesamiento simétrico, en nuestro caso máquinas con
doble procesador de tipo Pentium. Al comienzo, el controlador se enlaza con el
trabajador, se enlaza con sus controladores vecinos de arriba y abajo, y
establece una conexión con el maestro. El hardware subyacente para nuestra
configuración fue otro conmutador de 24 puertos, aunque los cables de cruce
podrían ser usados fácilmente con un costo de un adaptador de red adicional para
cada máquina. El anillo de datos utiliza el protocolo UDP para distribuir la
información actualizada dentro de sí mismo. Dado que los paquetes viajan
alrededor del anillo y regresan al transmisor, los paquetes perdidos pueden ser
detectados a través de un mecanismo de tiempo de espera y pueden ser reenviados.
En esta red se puede lograr una confiabilidad relativamente a bajo costo,
comparada a TCP/IP. En la implementación del conmutador, la multidifusión podría
ser posible, pero esto no ha sido investigado.
Por causa de que los eventos en diferentes esclavos pueden confiarse sobre
los otros, o manipular los mismos datos, la información debe ser
compartida entre los esclavos. Por esto, todos los esclavos se sincronizan sobre
un espacio de nombres global. Adicionalmente, el esclavo debe notificar al resto
antes de cambiar una expresión. Los esclavos también tienen la habilidad de
bloquear los otros eventos desde su ocurrencia, hasta que se notifica su
continuación. Finalmente, en el proceso de evaluar una expresión, nuevos eventos
pueden ser generados que son pasados de vuelta al maestro para su distribución.
Conceptos Destiny en Profundidad
Dos conceptos son claves para la comprensión de cómo trabajan los probadores
automáticos de teoremas tales como Destiny. El primero es el concepto de
respaldar un predicado. El segundo requiere entender un evento de reescritura y
cómo un motor procesa estos eventos.
Respaldando Predicados
Como se mencionó anteriormente, un predicado es la condición que debe ser
satisfecha con el fin de tomar una ruta particular en la ejecución de un
programa. Trabajando desde abajo (resultado final o estado) hacia arriba,
podemos componer una serie de estados y predicados para crear una expresión en
la parte superior (comienzo) representando la ruta completa de ejecución. Este
proceso puede ser aplicado a un bloque de código, o a la totalidad de un
programa. La Figura 8 ilustra la progresión original de un programa, y cómo los
predicados son respaldados a la versión final en la parte superior usando
notación de preorden. Nótese que es posible categorizar los vértices en niveles,
basados en el número de bifurcaciones, por ejemplo, y comprimir (converger
muchos vértices en uno) secuencialmente y sistemáticamente. Estas opciones
permiten a Destiny ofrecer variados niveles de información en grafos separados,
basados en los deseos del analista. La implementación actual y la lógica
matemática tras el respaldo de predicados está fuera del alcance de este
artículo.
Figura 8: Respaldando un predicado
El Motor de Reescritura
Una vez un programa o bloque de código ha sido respaldado, este debe ser
simplificado para producir resultados legibles e interpretables. El código
fuente Java autónomo (stand-alone) es la entrada original a Destiny. Este código
es compilado a código byte, y luego traducido a la forma funcional incorporada
en notación Lisp. El motor de reescritura usa entonces una base de datos de
reglas definidas por el usuario para hacer corresponder patrones con la
expresión con el fin de simplificarla. Por ejemplo, el motor de reescritura debe
ser educado primero en las reglas de adición asociativa, así que (+ x y) es
equivalente a (+ y x). Similarmente, éste debe entender cómo evaluar una
expresión, dígase (+ 2 3) como su valor calculado, 5. La reescritura se hace
desde arriba hacia abajo. En algún punto, no se corresponderán más reglas con
una expresión, y en ese momento es declarado estable. La persona que corre el
programa tiene la facultad, y es de hecho motivado, para manipular la base de
datos de reglas, adicionándole y reorganizando el orden en que las reglas son
aplicadas. En el ejemplo mostrado en la Figura 8, el motor de reescritura
debería evaluar la expresión como 22 en la parte superior.
Conclusiones
La prueba de teoremas no es un desarrollo novedoso ni reciente en matemáticas o
en ciencia de la computación. Sin embargo, el crecimiento de la potencia de la
computación moderna y la complejidad creciente de los problemas a ser resueltos
ha necesitado un nuevo enfoque a la solución de estos problemas. Las tres
principales ventajas de Destiny son el comienzo de un gran adelanto en la prueba
automática de teoremas. Primero, el trabajo es hecho interactivamente con un
analista, quien puede interpretar y extender los resultados generados por el
computador. Segundo, el procesamiento paralelo escalable puede ser empleado para
atacar cualquier problema de gran magnitud. Finalmente, Destiny está dirigido al
código Java, asignándole un conjunto de problemas sustancial y una máquina
abstracta portable y multiplataforma.
El desarrollo final y los tests extensivos todavía se mantienen antes de que
Destiny esté ampliamente disponible. Adicionalmente, se deben hacer tests de
forma acentuada para poner a punto la arquitectura subyacente. Sin embargo, los
conceptos introducidos en este nuevo diseño son poderosos y únicos, haciéndolo
un fuerte competidor como el próximo probador de teoremas de elección.
Referencias
-
1
- Bevier, W. A Verified Operating System Kernel. Ph.D. Th.,
University of Texas at Austin, 1987. University Microfilms and ftp://ftp.cs.utexas.edu/pub/boyer/diss/bevier.ps.Z.
-
2
-
Boyer, R.S. and J.S. Moore. A Computational Logic Handbook, Second
Edition. Academic Press, 1998.
-
3
-
Boyer, R.S. and J.S. Moore. "Proof Checking the RSA Public Key Encryption
Algorithm." American Mathematical Monthly 91, 3 (1984), 181-189.
-
4
-
Di Vito, B.L. Verification of Communications Protocols and Abstract
Process Models. Ph.D. Th., University of Texas at Austin, 1982. University
Microfilms.
-
5
- ANSI/IEEE: IEEE Standard for Software Verification and Validation.
ANSI/IEEE Std. 1012-1998, New York, 1998.
-
6
- Dahl, O., E. W. Dijkstra and C. A. Hoare. "Structured Programming."
Academic Press, New York, 1972.
-
7
-
Kaufmann, M. and J.S. Moore. "An Industrial Strength Theorem Prover
for a Logic Based on Common Lisp." IEEE Transactions on Software Engineering
23, 4 (April 1997), 203-213.
Biografía
Josiah Dykstra (dykstra@cs.hope.edu)
es un estudiante de pregrado en ciencia de la computación y double major
de música en el Colegio Hope en Holland, Michigan. Es un miembro
de la IEEE y está actualmente cumpliendo su segundo periodo como Presidente del
capítulo local de la ACM. Ha realizado pasantías con Gateway, Inc. y con la
Agencia de Seguridad Nacional (NSA) y ha dirigido investigaciones con la
Experiencia de Investigación para Programas de Pregrado de la NSF.
La investigación en Destiny fue dirigida en conjunto con la NSA.
Last Modified:
Location: www.acm.org/crossroads/espanol/xrds7-5/(article.html)