Abstract Certification of Java Programs in Rewriting Logic

Resum

En esta tesis se propone una metodología para la certi?cación de programas Java que está basadaen la lógica de reescritura, un marco formal lógico y semántico muy general, implementado e?cientemente en el lenguaje de programación funcional Maude. Se consideran propiedades de seguridad (safety), es decir, propiedades de un sistema que son de?nidas en términos de que no ocurranciertos eventos. Dichas propiedades se caracterizan como problemas de inalcanzabilidad en la lógica de reescritura. Las propiedades de seguridad (safety) se expresan en el estilo de JML, un lenguaje estándar de especi?cación de módulos Java. Con el ?n de obtener un procedimiento de decisión utilizamosm o de los con un número ?nito de estados que obtenemos mediante el uso de la interpretación abstracta. Partiendo de una especi?cación de la semántica de Java escrita en Maude, se desarrolla una semántica operacional abstracta con un número ?nito de estados, también escrita en Maude, que resulta apropiada para la veri?cación de programas. Como subproducto de la veri?cación se entrega un certi?cado de seguridad, que consiste en un conjunto de demostraciones basadas en reescritura, que pueden ser comprobadas fácilmente por el consumidor del código mediante el uso de un motor de reescritura estándar. La técnica de código portador de demostración (proof-carrying code) basada en abstracción, denominada JavaPCC, ha sido implementada y probada con éxito en varios ejemplos,lo cual de muestra la viabilidadd en uestro enfoque.