|
Resumen:
|
Las redes de Petri son un lenguaje formal muy adecuado para la modelizaci?on, an?alisis y verificaci?on de sistemas concurrentes con infinitos estados. En particular, son muy apropiadas para estudiar las propiedades de seguridad de dichos sistemas, dadas sus buenas propiedades de decidibilidad. Sin embargo, en muchas ocasiones las redes de Petri carecen de la expresividad necesaria para representar algunas caracter??sticas fundamentales de los sistemas que se manejan hoy en d??a, como el manejo de tiempo real, costes reales, o la presencia de varios procesos con un n?umero no acotado de estados ejecut?andose en paralelo. En la literatura se han definido y estudiado algunas extensiones de las redes de Petri para la representaci ?on de las caracter??sticas anteriores. Por ejemplo, las “Redes de Petri Temporizadas” [83, 10](TPN) incluyen el manejo de tiempo real y las ?-redes de Petri [78](?-PN) son capaces de representar un n?umero no acotado de procesos con infinitos estados ejecut?andose concurrentemente. En esta tesis definimos varias extensiones que re?unen estas dos caracter??sticas y estudiamos sus propiedades de decidibilidad. En primer lugar definimos las “?-Redes de Petri Temporizadas”, que re?unen las caracter??sticas expresivas de las TPN y las ?-PN. Este nuevo modelo es capaz de representar sistemas con un n?umero no acotado de procesos o instancias, donde cada proceso es representado por un nombre diferente, y tiene un n?umero no acotado de relojes reales. En este modelo un reloj de una instancia debe satisfacer ciertas condiciones (pertenecer a un intervalo dado) para formar parte en el disparo de una transici?on. Desafortunadamente, demostramos que la verificaci?on de propiedades de seguridad es indecidible para este modelo...
|
