Generación automática del árbol de transiciones reducido de un sistema, mediante el álgebra de procesos markovianos ROSA

Abstract

Es bien sabido que la Ingenier a Inform atica es una ciencia relativamente joven, la cual adolece de los t picos problemas de juventud tales como no tener completamente establecidos m etodos formales de prueba y/o veri caci on en sus desarrollos. Esto hace que pudieran aparecer fallos eventualmente graves, como consecuencia de usar un sistema de veri caci on denominado prueba y error donde, por muy minuciosos o por mucho esfuerzo que dediquemos, en muchos casos ser a inviable el coste de cubrir todos y cada uno de los posibles caminos que puede tomar una aplicaci on software. Debido a todo esto, contamos entre otros m etodos formales con algebras de procesos, las cuales consiguen recoger todos los posibles comportamientos por los que se puede regir una determinada aplicaci on software. En la actualidad los sistemas inform aticos est an presentes en cualquier ambito: control a ereo, control de ferroviario, centrales nucleares, : : :. En general, sistemas donde un fallo podr a tener grav simas consecuencias tanto humanas como econ omicas. Este factor, obliga a asegurar de forma s olida la correcci on y abilidad del sistema. Por otra parte, la detecci on de errores en el sistema durante las primeras etapas de su desarrollo, reduce enormemente el coste econ omico de su reparaci on. Las algebras de procesos, puesto que trabajan sobre la especi caci on del sistema, permiten detectar y ubicar errores con unos alt simos niveles de precisi on en etapas muy tempranas del desarrollo. Sin embargo, debido a la di cultad del formalismo, su uso no ha sido muy extendido. Por lo que surge la necesidad de construir herramientas que sean capaces de dar soporte al an alisis mediante su utilizaci on, dejando del lado del desarrollador, unicamente conocer la sintaxis del lenguaje, como si de un lenguaje de programaci on convencional se tratase. Por otra parte, el principal problema de las herramientas para algebras de procesos, es que sufren el conocido problema de explosi on de estados, que hace inviable su uso para el an alisis de sistemas muy grandes. Por ello el trabajo que ocupa esta tesis de m aster tiene como objetivo continuar el desarrollo de una herramienta basada en el algebra de procesos markonvianos ROSA, que es capaz de construir el sistema de transiciones etiquetado de un proceso, a trav es del cual se capturan todos los posibles comportamientos del mismo; as en aras de evitar la intratabilidad pr actica del problema que nos ocupa, nos planteamos reducir al m aximo el coste computacional de los algoritmos de an alisis en los que est an basados las algebras de procesos y con ello ofrecer un entorno m as usable a los desarrolladores de software. Concretamente, en esta tesis de m aster, se ha redise~nado uno de los algoritmos de an alisis de la herramienta y se han introducido mejoras que hacen que el algoritmo de construcci on del sistema de transiciones etiquetado, contenga un menor n umero de estados. Por otra parte con el n de ofrecer una interacci on m as amigable a los desarrolladores se ha dotado a la herramienta con un interfaz gr a co, que deja atr as a los cl asicos int erpretes de comandos y salidas en texto plano. A trav es del trabajo realizado y presentado en esta tesis de m aster, se ha conseguido desarrollar una herramienta que proporciona una v a m as usable para algebras de procesos y con la que se pretende alcanzar as parte del objetivo principal incluido en la tesis doctoral.