Repositorio RUIdeRA

Descripción e implementación de TPPAL: un álgebra de procesos temporizados y probabilísticos

Mostrar el registro sencillo del ítem

dc.contributor.author Pardo Mateo, Juan José
dc.date.accessioned 2010-10-27T09:50:55Z
dc.date.available 2010-10-27T09:50:55Z
dc.date.issued 2003
dc.identifier.isbn 84-8427-459-4
dc.identifier.uri http://hdl.handle.net/10578/952
dc.description.abstract Tradicionalmente, los diseñadores de sistemas concurrentes, antes de iniciar su trabajo, seleccionaban uno de los formalismos para ser utilizado y se centraban en ese, 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 realizada una especificación en uno de ellos, concretamente en un modelo algebraico, esta pueda 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 este muy ligado a restricciones temporales como son los sistemas de tiempo real. Con este nuevo modelo se intento 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 algebra, 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 estos 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ón, aunque tiene el inconveniente de dificultar el proceso de verificación formal. Ante las similitudes existentes entre los grafos de estados dinámicos y los autómatas temporizados, se realiza una traducción de los grafos a autómatas. Posteriormente se realiza una traducción de los términos del algebra a un modelo de redes de Petri, concretamente a redes de Petri con arcos temorizados, en el cual los Tokens tienen asociado un valor real no negativo, que indica el tiempo transcurrido desde su creación (su edad); y los arcos que van de un lugar a una transición estarán etiquetados por intervalos de tiempo, los cuales establecen restricciones a la edad de los Tokens que pueden ser usados para disparar la transición. En esta traducción se realiza una extensión temporizada de los resultados mostrados en algunos artículos, si bien hemos planteado además posibles extensiones de la traducción clásica explotando las características particulares del modelo de red de petri temporizada que hemos utilizado. Para finalizar la tesis se realiza una ampliación del modelo algebraico con operadores probabilísticos para la especificación de sistemas en los que su comportamiento se defina en función de unas probabilidades conocidas, y la traducción de los mismos a grafos de estados dinámicos probabilísticos. en_US
dc.format text/plain en_US
dc.language.iso es en_US
dc.publisher Ediciones de la Universidad de Castilla-La Mancha es_ES
dc.relation.ispartofseries Tesis doctorales;219
dc.rights info:eu-repo/semantics/openAccess en_US
dc.subject Matemáticas es_ES
dc.subject Informática es_ES
dc.title Descripción e implementación de TPPAL: un álgebra de procesos temporizados y probabilísticos es_ES
dc.type info:eu-repo/semantics/doctoralThesis en_US


Ficheros en el ítem

Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro sencillo del ítem

Buscar en RUIdeRA


Búsqueda avanzada

Listar

Mi cuenta