PDF de programación - Análisis y Verificación de Programas Modulares

UNIVERSIDAD POLIT¶ECNICA DE MADRID

FACULTAD DE INFORM ¶ATICA

An¶alisis y Verificaci¶on de

Programas Modulares

(Analysis and Verification of Modular

Programs)

Tesis Doctoral

Jes¶us Correas Fern¶andez

Licenciado en Inform¶atica

Junio de 2008

Departamento de Lenguajes y Sistemas

Inform¶aticos e Ingenier¶‡a del Software

Facultad de Inform¶atica

Tesis Doctoral

An¶alisis y Veriflcaci¶on de Programas

Modulares

presentada en la Facultad de Inform¶atica
de la Universidad Polit¶ecnica de Madrid

para la obtenci¶on del t¶‡tulo de

Doctor en Inform¶atica

Candidato: Jes¶us Correas

Licenciado en Inform¶atica
Universidad Polit¶ecnica de Madrid

Director: Germ¶an Puebla

Doctor en Inform¶atica
Licenciado en Inform¶atica

Madrid, Junio de 2008

UNIVERSIDAD POLITECNICA DE MADRID

Tribunal nombrado por el Magfco. y Excmo. Sr. Rector de la Universidad

Polit¶ecnica de Madrid, el d¶‡a. . . . . . de. . . . . . . . . . . . . . . . . . . . . . . . . . . de 200. . .

Presidente:

Vocal:

Vocal:

Vocal:

Secretario:

Suplente:

Suplente:

Realizado el acto de defensa y lectura de la Tesis el d¶‡a . . . . . . de. . . . . . . . . . . . . . . . . .
de 200. . . en la Facultad de Inform¶atica.

EL PRESIDENTE

LOS VOCALES

EL SECRETARIO

A Beatriz

Agradecimientos

En primer lugar, quiero expresar mi gratitud a mi director de tesis, Germ¶an
Puebla, y al director del Grupo de Investigaci¶on CLIP, Manuel Hermenegildo,
por todo el tiempo, energ¶‡a y recursos que me han permitido terminar esta tesis.
Adem¶as de su disponibilidad en todo momento, me han animado a continuar en
los momentos m¶as dif¶‡ciles y cuando m¶as lo necesitaba. Ha sido un gran honor
para m¶‡ formar parte de este grupo de investigaci¶on, y espero haber alcanzado el
nivel cient¶‡flco que se requiere para participar en las actividades que desarrolla
el grupo. Tambi¶en quiero agradecer a Paweˆl Pietrzak por su colaboraci¶on y su
amistad, que ha resultado en una fruct¶‡fera serie de trabajos en com¶un que forman
una parte fundamental de esta tesis, y que espero podamos continuar en otros
proyectos futuros.

Junto a ellos, los dem¶as coautores de los art¶‡culos y ponencias que forman
parte de esta tesis han contribuido a mi formaci¶on cient¶‡flca: Jos¶e Manuel G¶omez,
Manuel Carro, Francisco Bueno, Daniel Cabeza, Mar¶‡a Garc¶‡a de la Banda, Peter
Stuckey y Kim Marriott.

No puedo dejar de mencionar al resto de miembros del grupo CLIP, con los
que he compartido buenos tiempos y largas jornadas de trabajo. No dispongo de
espacio aqu¶‡ para referirme a todos ellos sin dejar a ninguno, pero quiero agradecer
en especial a Astrid Beascoa, que ha sido tantas veces la clave para terminar el
trabajo a tiempo y para compartir las diflcultades del d¶‡a a d¶‡a.

Tambi¶en quiero aprovechar la oportunidad para agradecer a los profesores
que me han invitado a estancias en sus respectivas universidades, por su apoyo
y acogida: John Gallagher en la Universidad de Roskilde, y Deepak Kapur en la
Universidad de Nuevo M¶ejico.

Por ¶ultimo, quiero agradecer a mis padres que me dieran lo que no ten¶‡an
para que yo pudiera llegar hasta aqu¶‡. Y todo esto hubiera sido imposible sin el
apoyo incondicional y la paciencia de Beatriz, a quien dedico esta Tesis.

Sinopsis

Existe un gran n¶umero de t¶ecnicas avanzadas de veriflcaci¶on y optimizaci¶on
est¶atica de programas que han demostrado ser extremadamente ¶utiles en la detec-
ci¶on de errores de programaci¶on y en la mejora de la eflciencia, y que tienen como
factor com¶un la necesidad de informaci¶on precisa de an¶alisis global del programa.
La interpretaci¶on abstracta es una de las t¶ecnicas de an¶alisis m¶as establecidas,
lo que ha permitido el desarrollo de m¶etodos innovadores para la veriflcaci¶on de
programas.

Por otra parte, uno de los desaf¶‡os m¶as importantes en la investigaci¶on in-
form¶atica actual consiste en mejorar la capacidad de detectar autom¶aticamente
errores en programas y asegurar que un programa es correcto respecto a una de-
terminada especiflcaci¶on, con el objetivo de producir software flable. Por ello, la
veriflcaci¶on de programas es un ¶area importante de investigaci¶on, y por ello pro-
porcionar t¶ecnicas avanzadas para detectar errores y veriflcar sistemas en progra-
mas reales complejos es una de las ¶areas m¶as relevantes en la industria inform¶atica
actual. Un enfoque interesante de la veriflcaci¶on de programas es la denominada
veriflcaci¶on abstracta, una t¶ecnica que tiene como objetivo la veriflcaci¶on de un
programa mediante sobre-aproximaciones de la sem¶antica concreta del programa.
Sin embargo, estos m¶etodos no son directamente aplicables a programas reales,
pues t¶ecnicas avanzadas como las mencionadas est¶an en muchos casos disponi-
bles como prototipos, y los avances conseguidos hasta ahora en esta direcci¶on
solamente han permitido su aplicaci¶on de modo restringido.

El objetivo de esta Tesis Doctoral es desarrollar t¶ecnicas de an¶alisis y veriflca-
ci¶on para su uso eflciente y preciso en grandes programas modulares o incomple-
tos y mostrar su factibilidad en sistemas reales. Con el fln de evaluar la utilidad
pr¶actica de las t¶ecnicas propuestas, los algoritmos resultantes han sido implemen-
tados e integrados en el sistema Ciao y se han comprobado experimentalmente,
lo que ha permitido aplicarlos en casos de estudio reales.

Resumen⁄

Introducci¶on y motivaciones

La descomposici¶on del c¶odigo de un programa en m¶odulos es una t¶ecnica funda-
mental en el proceso de desarrollo de software, pues permite construir programas
complejos a partir de m¶odulos sencillos.

A pesar de la importancia de la programaci¶on modular, existen muchas t¶ecni-
cas avanzadas de an¶alisis y veriflcaci¶on de programas (tales como dependencia del
contexto y polivarianza) que todav¶‡a no son aplicables a sistemas reales. Estas
t¶ecnicas han demostrado ser extremadamente ¶utiles en la detecci¶on de errores y
en la mejora de la eflciencia, pero desafortunadamente todav¶‡a est¶an orientadas
a programas pequeños sin las complejidades de los sistemas reales, tales como
interfaces con sistemas externos, bases de datos, librer¶‡as externas, componentes
implementados en otros lenguajes, as¶‡ como todas las caracter¶‡sticas que propor-
ciona la modularidad. Adem¶as, el ¶area de programaci¶on l¶ogica se ha visto afectado
por la ausencia (hasta el año 2000) de un est¶andar para describir la modularidad,
y que ha dado lugar a la coexistencia de varios enfoques en distintas implementa-
ciones del lenguaje. El objetivo de esta tesis consiste en hacer que estas t¶ecnicas
puedan utilizarse en programas l¶ogicos grandes, modularizados e incompletos.

Las t¶ecnicas de manipulaci¶on de programas tienen como factor com¶un la nece-
sidad de informaci¶on precisa de un an¶alisis global del programa. La interpretaci¶on
abstracta es una de las t¶ecnicas m¶as establecidas para obtener informaci¶on sobre
la ejecuci¶on de un programa sin ejecutarlo realmente. No obstante, para la apli-

⁄Este resumen de la Tesis Doctoral, presentada en lengua inglesa para su defensa ante un
tribunal internacional, es preceptivo seg¶un la normativa de doctorado vigente en la Universidad
Polit¶ecnica de Madrid.

I

caci¶on de las t¶ecnicas de an¶alisis existentes a programas complejos y modulares,
o bien se imponen restricciones al dominio abstracto para el que se analiza el
programa, o bien exigen renunciar a resultados tan precisos como los que se ob-
tienen para programas monol¶‡ticos pequeños. Esta tesis, como se ver¶a en detalle,
propone un marco de trabajo para el an¶alisis preciso de programas modulares sin
ninguna de estas dos limitaciones. Este marco de trabajo ha sido implementado
satisfactoriamente y evaluado mediante diversos experimentos que han permitido
comparar las distintas conflguraciones de los par¶ametros del sistema. Adem¶as se
han realizado experimentos de rean¶alisis incremental de programas modulares en
presencia de modiflcaciones en algunos de los m¶odulos del programa.

Por otra parte, uno de los desaf¶‡os m¶as importantes en la investigaci¶on in-
form¶atica actual consiste en mejorar la capacidad de detectar autom¶aticamente
errores en programas y asegurar que un programa es correcto respecto a una
determinada especiflcaci¶on, con el objetivo de producir software flable. Por ello,
la veriflcaci¶on de programas es un ¶area importante de investigaci¶on. En el caso
habitual de programas desarrollados por un equipo de programadores, es espe-
cialmente interesante el uso de t¶ecnicas de an¶alisis y depuraci¶on que puedan con-
siderar programas incompletos, de forma que se permita su uso aun cuando parte
del programa no est¶e disponible. Esta caracter¶‡stica permitir¶‡a utilizar t¶ecnicas
avanzadas en el ciclo de edici¶on-compilaci¶on-pruebas en fases anteriores a las que
se han utilizado hasta ahora. Sin embargo, resulta habitual que los enfoques ac-
tuales de veriflcaci¶on de programas requieran que tanto el c¶odigo que compone
el programa como una especiflcaci¶on completa del mismo est¶en disponibles para
el sistema veriflcador. Este requerimiento no es realista para programas grandes
y complejos, y en particular en aquellos sistemas desarrollados hace tiempo, de
los que ni siquiera se dispone de una documentaci¶on de usuario completa. La
mejor soluci¶on en estos casos consiste en permitir una especiflcaci¶on parcial del
programa, y utilizar t¶ecnicas de an¶alisis avanzadas para inferir lo que falta en la
especiflcaci¶on. Posteriormente, esta informaci¶on puede utilizarse para veriflcar la
correcci¶on del programa respecto a la especiflcaci¶on parcial mencionada anterior-
mente. Este planteamiento resulta, evidentemente, en una fase de veriflcaci¶on m¶as
d¶ebil, pues se supone que los aspectos del programa para los que no se dispone de
especiflcaci¶on est¶an correctamente satisfechos por el c¶odigo. No obstante, la in-
formaci¶on inferida puede utilizarse para veriflcar la correcci¶on de la especiflcaci¶on

II

disponible.

Esta tesis utiliza