Model checking for verification of avionics software

• Autores: Pedro Manuel de la Cámara Cruz
• Directores de la Tesis: María del Mar Gallardo Melgarejo (codir. tes.) , Pedro Merino Gómez (codir. tes.)
• Lectura: En la Universidad de Málaga ( España ) en 2013
• Idioma: español
• Tribunal Calificador de la Tesis: Ernesto Pimentel Sánchez (presid.) , Manuel Díaz Rodríguez (secret.) , Alberto Lluch Lafuente (voc.) , Fernando Cuartero Gómez (voc.) , Elvira Albert (voc.)
• Texto completo no disponible (Saber más ...)
• Resumen

  • El objetivo de la tesis es la verificación de software de avionica utilizando Model Checking. El software a verificar sera ejecutable sobre un RTOS basado en el estándar ARINC 653. El la herramienta de Model Checking es SPIN.

    La aproximación propuesta consiste en tres pasos: 1.- Una herramienta extrae automaticamente modelos PROMELA + C a partir de codigo C 2.- Los modelos extraidos se integran con un modelo pre-existented del RTOS ARINC 653.

    3.- El modelo integrado se verifica con SPIN.

    Se han desarrollado tres lineas de trabajo: 1.- Extracción de modelos: Diseño de herramientas y métodos para la extracción de modelos PROMELA a partir de codigo C, y su posterior integración con un modelo pre-existnte de RTOS.

    2.- Modelado de un RTOS ARINC 653.

    3.- Técnicas de Optimizacion para reducir los recursos que SPIN utiliza durante la verificacion.

    Las lineas de trabajo han arrojado los siguientes resultados: 1.- Se ha demostrado la viabilidad de extraer modelos mediante la implementacion de una herramienta.

    2.- Se ha demostrado la viabilidad de tener modelos de OS separados de las aplicaciones mediante un ejemplo de Socket API.

    3.- Se ha creado un modelo de los servicios ARINC 653 más relevante, incluyendo Planificacion de procesos y gestión de tiempo.

    4.- Se ha verificado la corrección del modelo de RTOS ARINC 653 mediante casos de test oficiales.

    5.- Se ha desarrollado una técnica de optimización, combinando Abstract Matching con análisis estáticos, para que SPIN ignore las variables irrelevantes durante la verificación.

    Las principales contribuciones de este trabajo son: 1.- La aproximación de extraer modelos a partir de codigo fuente mientras que se modela el RTOS.

    2.- La demostración de los beneficios de utilizar SPIN en la verificacion.

    3.- La viabilidad de verificar aplicaciones de avionica complejas.

    4.- El metodo para modelar el tiempo real con SPIN.

    5.- La propuesta de verificar el modelo de RTOS mediante casos de test oficiales ARINC 653.

    6.- El metodo que utiliza Abstract Matching de manera agresiva para ignorar la variables irrelevantes durante la verificación con SPIN.