Tratamiento formal de sistemas con requisitos de tiempo real críticos

Laburpena

Esta tesis se enmarca dentro de la disciplina del tratamiento formal de sistemas con requisitos de tiempo real críticos, una vez han sido completa o parcialmente resueltos los principales problemas teóricos en el ámbito de los métodos formales con requisitos de dichas características, el objetivo de este trabajo de tesis es ligeramente diferente. Con el fin de mejorar la calidad del software, es nuestra intención con jugar dos soluciones de diferente naturaleza: la formalización del proceso software y una estructura de proceso software iterativa e incremental, cordinando la corrección de los métodos formales y lo flexible de un ciclo de vida que no congela los requisitos en fases tempranas y divide la complejidad. El objetivo central de esta tesis es la extensión de la metodología formal SCTL/ROS, conjugando ambos enfoques, para la aplicación al ámbito de los sistemas con requisitos de tiempo real críticos. En base a este objetivo, se define el modelo de estados MUS-T, y la lógica temporal SCTL-T; extensiones con tiempo denso del modelo MUS y la lógica SCTL. Además se proporcionan métodos de decisión orientados K análisis y a sintesis que articulan el modelo de ciclo de vida propuesto en la producción de este tipo de sistemas. Para garantizar la eficiencia de la metodología se propone un algoritmo de minimización. Por último, para su validación se presenta un caso de estudio en el estado del arte de los sistemas de tiempo real críticos.