La herramienta KeY se utiliza en la verificación formal de programas Java . Acepta especificaciones escritas en Java Modeling Language en archivos fuente de Java. Estos se transforman en teoremas de lógica dinámica y luego se comparan con la semántica de programa que también se define en términos de lógica dinámica. KeY es significativamente poderoso ya que admite pruebas de corrección tanto interactivas (es decir, a mano) como totalmente automatizadas. Los intentos fallidos de prueba se pueden utilizar para una depuración más eficiente o una prueba basada en verificación . Ha habido varias extensiones de KeY para aplicarlo a la verificación de programas C osistemas híbridos . KeY es desarrollado conjuntamente por el Instituto de Tecnología de Karlsruhe , Alemania; Technische Universität Darmstadt , Alemania; y la Universidad Tecnológica de Chalmers en Gotemburgo, Suecia, y cuenta con la licencia GPL .
Desarrollador (es) | Instituto de Tecnología de Karlsruhe , Technische Universität Darmstadt , Universidad de Tecnología de Chalmers |
---|---|
Lanzamiento estable | 2.8.0 / 18 de diciembre de 2020 [1] |
Escrito en | Java |
Sistema operativo | Linux, Mac, Windows, Solaris |
Disponible en | inglés |
Tipo | Verificación formal |
Licencia | GPL |
Sitio web | www |
Descripción general
La entrada habitual del usuario a KeY consiste en un archivo fuente Java con anotaciones en JML. Ambos se traducen a la representación interna de KeY, la lógica dinámica . A partir de las especificaciones dadas, surgen varias obligaciones de prueba que deben cumplirse, es decir, debe encontrarse una prueba. Para ello, el programa se ejecuta simbólicamente con los cambios resultantes en las variables del programa almacenadas en las llamadas actualizaciones . Una vez que el programa se ha procesado por completo, queda una obligación de prueba lógica de primer orden . En el corazón del sistema KeY se encuentra un demostrador de teoremas de primer orden basado en el cálculo secuencial , que se utiliza para cerrar la demostración. Las reglas de interferencia se capturan en los llamados taclets que consisten en un lenguaje propio y simple para describir los cambios en una secuencia.
Tarjeta Java DL
La base teórica de KeY es una lógica formal llamada Java Card DL. DL son las siglas de Dynamic Logic. Es una versión de una lógica dinámica de primer orden adaptada a los programas de Java Card. Como tal, por ejemplo, permite declaraciones (fórmulas) como, que intuitivamente dice que la poscondición debe mantenerse en todos los estados del programa accesibles mediante la ejecución del programa Java Card en cualquier estado que satisfaga la condición previa . Esto es equivalente aen el cálculo de Hoare si y son puramente de primer orden. La lógica dinámica, sin embargo, extiende la lógica de Hoare en el sentido de que las fórmulas pueden contener modalidades de programa anidadas como, o que es posible la cuantificación sobre fórmulas que contienen modalidades. También existe una modalidad dualque incluye rescisión . Esta lógica dinámica puede verse como una lógica multimodal especial (con un número infinito de modalidades) donde para cada bloque de Java hay modalidades y .
Componente de deducción
En el corazón del sistema KeY se encuentra un demostrador de teoremas de primer orden basado en un cálculo secuencial . Un secuente tiene la forma dónde (supuestos) y (proposiciones) son conjuntos de fórmulas con el significado intuitivo que se mantiene cierto. Por medio de la deducción , se demuestra que un secuente inicial que representa la obligación de prueba es construible a partir de axiomas fundamentales de primer orden (como la igualdad).
Ejecución simbólica de código Java
Durante eso, las modalidades del programa se eliminan mediante ejecución simbólica . Por ejemplo, la fórmula es lógicamente equivalente a . Como muestra este ejemplo, la ejecución simbólica en lógica dinámica es muy similar al cálculo de las condiciones previas más débiles . Ambas cosas y esencialmente denotan lo mismo, con dos excepciones: en primer lugar, es una función de algún metacálculo mientras realmente es una fórmula del cálculo dado. En segundo lugar, la ejecución simbólica se ejecuta a través del programa hacia adelante como lo haría una ejecución real. Para guardar los resultados intermedios de las asignaciones, KeY introduce un concepto llamado actualizaciones , que son similares a las sustituciones pero solo se aplican una vez que la modalidad del programa se ha eliminado por completo. Sintácticamente, las actualizaciones consisten en asignaciones paralelas (sin efectos secundarios) escritas entre llaves delante de una modalidad. Un ejemplo de ejecución simbólica con actualizaciones: se transforma en en el primer paso y para en el segundo paso. Entonces, la modalidad está vacía y la "aplicación hacia atrás" de la actualización a la condición posterior produce una condición previa en la que podría tomar cualquier valor.
Ejemplo
Supongamos que uno quiere demostrar que el siguiente método calcula el producto de algunos números enteros no negativos y .
int foo ( int x , int y ) { int z = 0 ; while ( y > 0 ) if ( y % 2 == 0 ) { x = x * 2 ; y = y / 2 ; } más { y = y / 2 ; z = z + x ; x = x * 2 ; } return z ; }
Uno así comienza la prueba con la premisa y la conclusión que se mostrará . Tenga en cuenta que los cuadros de cálculos secuenciales generalmente se escriben "al revés", es decir, el secuente inicial aparece en la parte inferior y los pasos de deducción van hacia arriba. La prueba se puede ver en la figura de la derecha.
Características adicionales
Depurador de ejecución simbólica
El depurador de ejecución simbólica visualiza el flujo de control de un programa como un árbol de ejecución simbólico que contiene todas las rutas de ejecución factibles a través del programa hasta cierto punto. Se proporciona como complemento a la plataforma de desarrollo Eclipse .
Generador de casos de prueba
KeY se puede utilizar como una herramienta de prueba basada en modelos que puede generar pruebas unitarias para programas Java. El modelo del cual se derivan los datos de prueba y el caso de prueba consiste en una especificación formal (proporcionada en JML ) y un árbol de ejecución simbólico de la implementación bajo prueba que es calculado por el sistema KeY.
Distribución y variantes del sistema KeY
KeY es un software gratuito escrito en Java y con licencia GPL . Se puede descargar desde el sitio web del proyecto en origen; actualmente no hay binarios precompilados disponibles. Como otra posibilidad, KeY se puede ejecutar directamente a través del inicio web de Java sin necesidad de compilación e instalación.
KeY-Hoare
KeY-Hoare se basa en KeY y presenta un cálculo Hoare con actualizaciones de estado. Las actualizaciones de estado son un medio para describir las transiciones de estado en una estructura de Kripke . Este cálculo puede verse como un subconjunto del que se usa en la rama principal de KeY. Debido a la simplicidad del cálculo de Hoare, esta implementación está destinada esencialmente a ejemplificar los métodos formales en las clases de pregrado.
KeYmaera / KeYmaeraX
KeYmaera [1] (anteriormente llamado HyKeY) es una herramienta de verificación deductiva para sistemas híbridos basada en un cálculo para la lógica dinámica diferencial dL [2] . Extiende la herramienta KeY con sistemas de álgebra computarizada como Mathematica y los algoritmos y estrategias de prueba correspondientes, de modo que se puede utilizar para la verificación práctica de sistemas híbridos .
KeYmaera se ha desarrollado en la Universidad de Oldenburg y la Universidad Carnegie Mellon . El nombre de la herramienta fue elegido como homófono de Quimera , el animal híbrido de la mitología griega antigua.
KeYmaeraX [3] desarrollado en la Universidad Carnegie Mellon es el sucesor de KeYmaera. Ha sido completamente reescrito.
Clave para C
Clave para C es una adaptación del sistema de llave a Misra C , un subconjunto del lenguaje de programación C . Esta variante ya no es compatible.
ASMKeY
También hay una adaptación para usar KeY para la ejecución simbólica de Abstract State Machines , que fue desarrollada en ETH Zürich . Esta variante ya no es compatible; se puede encontrar más información en el enlace web a continuación.
Fuentes
- Verificación de software orientado a objetos: el enfoque clave . Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt (Eds.). Springer , 2007. ISBN 978-3-540-68977-5 .
- Verificación de software deductivo: el libro clave: de la teoría a la práctica . Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, Mattias Ulbrich (Eds.). Springer , 2016. ISBN 978-3-319-49812-6
- Una comparación de herramientas para enseñar la verificación formal de software . Ingo Feinerer y Gernot Salzer. Springer , 2008
- Programación con pruebas: enfoques basados en el lenguaje para corregir totalmente el software . Aaron Stump. Software verificado: teorías, herramientas y experimentos, 2005.
- Alta garantía (para seguridad o protección) y software libre / de código abierto (FLOSS) . David Wheeler, 2009
enlaces externos
- Página de inicio del proyecto KeY
- Página de inicio de KeYmaera
- Página de inicio de KeYmaeraX
- ^ "Descargar - The KeY Project" . key-project.org . Consultado el 13 de abril de 2021 .