Resumen de Model checking for verification of avionics software

Pedro Manuel de la Cámara Cruz

• 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.