Descripción e implementación de Tppalun algebra q de procesos temporizados y probabilísticos

Résumé

Tradicionalmente, los diseñadores de sistemas concurrentes, antes de iniciar su trabajo, seleccionaban uno de los formalismos para ser utilizado y se centraban en ése, descartando el resto de modelos. Con esto se estaban descartando las ventajas que los otros modelos podrían aportar a su trabajo. Ante esta situación, parece interesante el tener una relación definida entre los diferentes modelos, de modo que una vez realizaba una especificación en uno de ellos, concretamente en un modelo algebraico, ésta puede ser transformada a otro de los modelos, dependiendo de las necesidades del momento, y de las facilidades que cada uno de los modelos proporcione para el estudio de unas determinadas propiedades. Con esta idea en la cabeza, se inicio el trabajo que ha culminado en esta tesis, en la cual, en primer lugar se presenta el modelo algebraico base definido, el cual es un modelo temporizado. Este modelo está basado en LOTOS, añadiendo algunos operadores temporizados, que permitiesen la especificación de los sistemas cuyo comportamiento esté muy ligado a restricciones temporales como son los sistemas de tiempo real. Con este nuevo modelo se intentó recoger las mejores características de algunos de los modelos se intentó recoger las mejores características de algunos de los modelos existentes en un único modelo. Tras definir el modelo algebraico base, el primer modelo al que se traduce este álgebra, fue el modelo de grafos de estados dinámicos. Este modelo está basado en los autómatas temporizados definidos por Alur y Dill, aunque posee algunas diferencias con respecto a los autómatas entre las que podemos destacar, el uso de los relojes, que en nuestro caso no serán inicializados a 0 por ninguna transición, sino que éstos son sincronizados con el instante de tiempo del instante en que se ejecuta la acción. Ello nos permite conocer de una forma inmediata el tiempo consumido por cada componente de la especificació