Medistam-rtmetodología de diseño y análisis de sistemas de tiempo real

Resumen

La complejidad creciente de los sistemas de tiempo real (STR) hace cada vez más difícil su tarea de desarrollo, Los desarrolladores se enfrentan a la construcción de sistemas concurrentes que interaccionan entre sí bajo restricciones de tiempo críticas y que, además, la mayoría de las veces, están sometidos a un entorno externo impredecible. En esta tesis presentamos un nuevo enfoque metodológico, denominado MEDISTAM-RT (Método de Diseño de Sistemas basado en la Transformación Analítica de Modelos del Tiempo Real), para el diseño y análisis correcto de sistemas de tiempo real. La metodología MEDISTAM-RT está fundamentada en la transformación de modelos semiformales basados en UML y UML-RT (que hemos denominado modelos MEDISTAM-RT), en especificaciones formales en CSP+T. Esta propuesta metodológica permite el uso de UML para el modelado de los requisitos temporales de un STR, así como, garantizar la consistencia del comportamiento de los diferentes componentes del sistema en las que aparezca recogida su especificación. En particular, se ha puesto especial énfasis en el aseguramiento de la consistencia temporal (esto es, la sincronización correcta entre los diferentes componentes de un STR). Además, la propuesta realizada posibilita la verificación formal del sistema mediante el lenguaje basado en álgebra de procesos CSP+T (extensión de tiempo real para CSP), partiendo del lenguaje semiformal UML-RT. Para ello, por un lado, se ha enriquecido la sintaxis de UML-RT con anotaciones inspiradas en CSP+T para la descripción de restricciones temporales. Asimismo, se ha definido un conjunto de reglas de transformación que permiten derivar sistemáticamente una especificación formal en términos de procesos CSP+T, a partir de modelos de MEDISTAM-RT. Adicionalmente, se han definido técnicas para garantizar la consistencia entre los diferentes modelos del sistema objeto de diseño con la metodología. Por otro lado, se ha definido una semántica denotacional para el lenguaje CSP+T con objeto de permitir especificar y verificar requisitos temporales y propiedades importantes de corrección de sistemas de tiempo real, como son las propiedades de seguridad y vivacidad. Por último, se ha aplicado la metodología a un caso de estudio concreto consistente en el análisis y modelado de un robot de prensado para demostrar la facilidad de uso y la corrección de la especificación del sistema obtenido,, así como comprobar la verificabilidad de los requisitos temporales