Inicio   >   Demostradores   >   KINDSPEC

KINDSPEC

Demostrador|vrain

Descripción
KindSpec infiere automáticamente contratos software a partir de programas C
Miembro
dirección
Camino de Vera S/N
Provincia
Valencia

INFORMACIÓN DEL DEMOSTRADOR

DESCRIPCIÓN

KindSpec es una herramienta para la inferencia automática de contratos software a partir de programas escritos en un fragmento significativo del lenguaje C llamado KernelC. KernelC soporta estructuras de datos dinámicas basadas en punteros y manipulación de la pila. KindSpec toma como entrada un programa y el usuario debe especificar cuál es el método (llamado modificador) para el que quiere inferir el contrato software. Una vez especificado, KindSpec genera automáticamente un contrato usando los métodos observadores (que tienen un valor de retorno) del propio program. El contrato inferido consiste en axiomas lógicos que expresan precondiciones y poscondiciones que definen el comportamiento entrada/salida del método objeto. Al usar métodos del propio programa como componentes de los asertos, resultan fácilmente comprensible por parte del desarrollador. Los axiomas inferidos pueden servir tanto para la documentación del código como para la detección de carencias o errores en el sistema cuando los asertos inferidos no son los esperados. La herramienta puede generar informes sobre el contrato software final, estadísticas, y almacenar el contrato en un objeto serializado que puede ser usado por otras herramientas.

POSIBILIDADES

El método de inferencia de KindSpec se basa en la técnica de ejecución simbólica y en la interpretación abstracta para podar el árbol de ejecución simbólica cuando tenemos ramas infinitas originadas por bucles y por la recursión. Existen distintas alternativas de configuración asociadas a esta tecnología. Podemos establecer que se use aliasing en la ejecución simbólica para así poder capturar propiedades de estructuras de datos cíclicas. También podemos seleccionar un dominio abstracto que permita realizar una poda del árbol más precisa que el uso de una profundidad máxima. El uso de abstracciones permite detectar patrones en los bucles que pueden dar lugar a axiomas que representen un determinado comportamiento. Debido a la abstracción, no podremos garantizar la corrección de algunos axiomas, que se anotan como candidatos hasta que puedan ser verificados o descartados en el proceso de refinamiento que puede ejecutarse tras la inferencia. Desde el apartado de refinamiento, el usuario puede seleccionar los axiomas candidatos que quiera refinar bien mediante un proceso de falsificación (para descartarlos por ser incorrectos) bien mediante un proceso de verificación (de forma que pasarán a formar parte del contrato). Asociado al proceso de verificación, se realiza una generalización y simplificación de axiomas ya que es posible que con la introducción de nuevos axiomas se puedan definir axiomas más generales que subsuman a varios axiomas del contrato. En este caso, los axiomas subsumidos se eliminan del contrato dejando solo el axioma general. Gracias a este proceso podemos obtener especificaciones más compactas y fáciles de comprender por el usuario.

HABILITADOR TECNOLOGICO

Inteligencia Artificial y Computación
Data security and privacy technologies

Program verification, safety analysis, provable security. Protocol crypto-analysis. Automated analysis, modeling, verification, synthesis, learning, debugging and optimization of complex systems and models