Análisis de alternativas para resolver problemas de tiempo real

José L. Pasciaroni.

2001.

123 h. : ilustraciones ; 30 cm. .

Tesis--Universidad Nacional del Sur, 2001.

Resumen: Existe un interés creciente en Ciencias de la Computación por el estudio y tratamiento de nociones temporales. Siempre que se trate de modelar un sistema dinámico donde exista la noción de cambio o evolución, van a existir nociones temporales para representar su variación a través del tiempo. Algunas áreas de Ciencias de la Computación que requieren métodos eficientes y seguros para la solución de problemas en los que se utiliza información temporal son las bases de datos temporales, sistemas distribuidos, diseño de aplicaciones multimediales e Inteligencia Artificial. Otra área en la que se torna imprescindible la consideración del tiempo es la implementación de sistemas que actúan en tiempo real. Los procesadores se usan para especificar, desarrollar, monitorear y controlar sistemas con restriciones críticas, por ejemplo: sistemas reactivos, problemas de sincronización en entornos industriales, control de vuelos, plantas nucleares, redes telefónicas y pacientes en hospitales. En tales casos, para cumplir su propósito en forma adecuada, los sistemas deben satisfacer lo que se denomina "restricciones de tiempo real". Puede comprobarse a través de la literatura que existe una gran diversidad de ofertas al momento de seleccionar una para resolver problemas como los anteriores. Por otra parte, las características del mismo tienen una influencia fuerte al momento de determinar cual debe utilizarse para resolverlo. Como consecuencia de esto no existe una en especial que resulte claramente preferible al resto en cualquier circunstancia. Entre ellas podemos citar a las redes de Petri temporales ([Men96],[MLC96],[men83] y [Men85]), autómatas finitos temporales [Alu98], lenguajes de programación como Ada [Pyl81], álgebra temporal de procesos tal como CSP [RR88], Modecharts [JM87] y lógicas para tiempo real [AH93]. Sea cual fuere el área de aplicación, conocer las virtudes y limitaciones de una herramienta tiene un gran impacto en la aplicación de la formalización adoptada. Por ejemplo, decisiones simples en torno a las hipótesis consideradas pueden tener un gran impacto en la eficiencia de la implementación. Por lo tanto es valioso conocer el comportamiento general de las herramientas disponibles para resolver problemas con determinadas características. Dado un grupo de ellas es útil conocer cual es su capacidad expresiva, lo que permite determinar si un problema puede resolverse o no con el formalismo en cuestión. Finalmente, cuandop hay más de una posible, también es valioso contrastar su complejidad computacional, expresividad y facilidad de utilización. El número de formalismos que facilitan el modelaje, especificación y prueba de propiedades temporales de sistemas reactivos, se incrementó apreciablmente durante los últimos años. Las propuestas con diferentes sintaxis y semántica crearon muchas veces confusión no solo debido a una notación diferente sino a las distintas presunciones al modelar tiempo y computación, lo que vuelve a la comparación una tarea no trivial. Las investigaciones asociadas a ésta tesis tienen por objetivo exponer el formalismo de algunas de las herramientas más conocidas o que mayor desarrollo han experimentado en los últimos años y realizar un análisis comparativo entre ellas. Los resultados aumentarán el conocimiento acerca de los sistemas y la correspondiente obtención de implementaciones basadas en los mismos.ORGANIZACION: En el capítulo 1 se presentarán las redes de Petri temporales como alternativa donde sea importante contar con un medio de establecer determinadas restricciones a ciertas componentes del sistema modelado. Como se verá, estas redes son una herramienta para la especificación y estudio de sistemas, especialmente por su aptitud de modelar problemas en los cuales se puede aprovechar su capacidad de representar concurrencia o paralelismo de actividades, particularmente en aquellos donde se manifiesta flujo de información o de recursos. En el capítulo 2 se mostrarán los autómats temporales como una herramienta práctica de verificación automática de sistemas reactivos complejos tal como controladores embebidos o protocolos de red. como se verá, la forma de descubrir inconsistencias mediante la técnica denominada "Model-checking", se basa en la comparación entre una descripción de alto nivel del sistema bajo análisis y los requerimientos de correctitud lógica (capítulo 3).Finalmente, en el capítulo 3 se considerará la aplicación de las lógicas temporales de tiempo real a la verificación de propiedades de un sistema y a la especificación de los mismos. Se examinarán los formalismos que se basan en autómatas y en lógicas, poniéndolos en perspectiva mediante la utilización de una semántica común, lo cual permitirá realizar su comparación. CALIFICACION DEPARTAMENTO DE GRADUADOS Calificación de la defensa oral: Sobresaliente - 10 (diez) Fecha: 29/08/01

Incluye referencias bibliográficas.