Técnicas para el análisis de la consistencia de modelos en el desarrollo de software embarcado

Resumen

Uno de los grandes problemas que tienen las empresas que desarrollan sistemas intensivos en software es el elevado coste que suponen las tareas de verificación y de mantenimiento correctivo asociado. En los sistemas con software embarcado certificable (bajo la norma RTCA DO-178B [DO-178B]) este asunto es especialmente crítico. En software para aviación el nivel de verificación exigido requiere de la utilización de complejas infraestructuras de pruebas que van desde bancos de ensayo software-software, pasando por bancos de integración hardware-software hasta ensayos en avión en tierra y ensayos en vuelo. Además se requiere la utilización de costosas herramientas de análisis de código para demostrar ante las autoridades certificadoras aspectos como la cobertura estructural o el WCET (Worst Case Execution Time). Una de las estrategias más prometedoras para tratar de minimizar este coste es el paradigma de Ingeniería Basada en Modelos (MBE). El principio básico de MBE es dedicar un esfuerzo mayor a la elaboración de los modelos de alta calidad para que la etapa de construcción sea lo más automatizada posible y el producto final contenga el mínimo número de errores derivados de una inadecuada elaboración del diseño. Para conseguir un modelo de alta calidad es necesario poner énfasis en la verificación de los modelos. La verificación de modelos requiere por un lado de notaciones eficaces que permitan representar características relevantes de los sistemas y por otro de mecanismos ágiles de evaluación de los modelos. La idea es que cuanto antes se detecten y corrijan errores, menos costosa será la construcción de los sistemas. La hipótesis planteada en esta Tesis es que los modelos de arquitectura poseen una serie de propiedades que son susceptibles de ser evaluadas en etapas muy tempranas del diseño, en las que hay muy pocos detalles del diseño detallado o de la plataforma de ejecución. Estas propiedades pueden emplearse para establecer criterios de aceptación que conformen esquemas de decisión de alternativas de diseño. En el contexto de los sistemas embarcados de tiempo real los aspectos de concurrencia de tareas son de especial relevancia porque tales sistemas son esencialmente reactivos a eventos y los eventos llegan al sistema de forma aleatoria y han de ser tratados por éste de forma simultánea. Los problemas de concurrencia de los sistemas reactivos no son problemas aislados sino que con frecuencia están relacionados entre si. Una de las primeras contribuciones de esta Tesis es precisamente una taxonomía de problemas de los sistemas concurrentes donde se ponen de manifiesto las interrelaciones entre estos problemas. Uno de los problemas de especial relevancia en el contexto de la concurrencia es el interbloqueo de tareas, por sus implicaciones desde el punto de vista de cumplimiento con requisitos de safety. En este ámbito, esta Tesis Doctoral propone como objetivo principal una nueva estrategia para valorar el riesgo de interbloqueo presente en un modelo de arquitectura software. Esta estrategia está basada en una caracterización del problema de interbloqueo adaptada a un nivel de abstracción elevado. La caracterización se realiza mediante la detección de ciclos de dependencia de tareas, complementada con la detección de patrones de interbloqueo estáticos y dinámicos. La estrategia de tratamiento del interbloqueo propuesta en esta Tesis no se enmarca en sentido estricto dentro de ninguna de las tres categorías clásicas de tratamiento del interbloqueo (prevención, evitación y detección), dado que no tiene como objetivo abordar el problema a bajo nivel sino identificar su riesgo potencial para ayudar a los diseñadores a tomar decisiones en las primeras etapas del diseño de un sistema de tiempo real intensivo en software. El objetivo secundario de la Tesis es demostrar que es posible poner en práctica los principios de la Ingeniería Basada en Modelos con esfuerzos de diseño y de desarrollo reducidos. Para la puesta en práctica de la estrategia propuesta se ha desarrollado un prototipo de herramienta que implementa la nueva caracterización de interbloqueo. Para validar los algoritmos soportados por la herramienta se ha usado como prueba la herramienta Cheddar [Singhoff, 2004]. Para demostrar la viabilidad de la estrategia y la utilidad de la herramienta se han usado los siguientes tres casos de estudio: * Sistema de control de un ascensor: Este caso de estudio aporta como valor añadido que representa un sistema completo frente a los otros casos donde sólo se representa una parte. * Sistema de gestión automática de sintonización de equipos de comunicaciones de la aviónica de un avión de transporte militar: Este caso de estudio aporta como valor añadido que se proporcionan alternativas de diseño y una estimación de ahorro en esfuerzo de verificación asociado a la evaluación temprana del riesgo de interbloqueo. * Sistema de control de un rover de exploración planetaria: Este caso de estudio aporta como valor añadido que se compara el resultado obtenido con el de la aplicación de métodos formales. Estos casos de estudio son diseños reales que se han capturado en la notación PPOOA-UML y se han evaluado de acuerdo con la nueva caracterización. Además de cumplir con el objetivo demostrar la viabilidad de la aproximación, estos casos de estudio han sido de gran ayuda durante el proceso de depuración de las métricas elegidas para la caracterización. Finalmente los casos de estudio han servido para mostrar las guías para tomar decisiones a la hora de valorar alternativas de diseño.