Model checking for verification of avionics software

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.