Redes de Petri móviles para la especificación y verificación de propiedades de seguridad en sistemas ubicuos

Abstract

Las redes de Petri son un formalismo presentado por primera vez en la tesis de Carl Adam Petri para el estudio de sistemas concurrentes, Desde su aparición hace ya más de cuatro décadas han aparecido numerosos trabajos que han desarrollado una estable teoría para la especificación y verificación de sistemas concurrentes mediante redes de Petri. Factores como su representación gráfica y los numerosos resultados de decidibilidad para problemas indecidibles en otros formalismos más expresivos son sin duda parte de los motivos que han contribuído al éxito del que han gozado las redes de Petri. Sin embargo, la teoría clásica de redes se enfrenta al desafío de adecuarse a las nuevas necesidades de los sistemas informáticos que los ingenieros diseñan en la actualidad. Un claro ejemplo de estas nuevas necesidades son los sistemas distribuídos y móviles, en los que conceptos como localidad y conectividad cobran gran importancia. Un paso más allá están los sistemas ubicuos, definidos de manera un tanto difusa, que comparten la particularidad de estar formados por componentes con poca capacidad de cálculo que se comunican a través de redes establecidas específicamente para cada comunicación, lo que dificulta el diseño de sistemas ubicuos seguros. En esta tesis nos centramos en dos aspectos de vital importancia en los sistemas ubicuos, como son la coordinación y la seguridad. El primer objetivo de la tesis es el de extender el modelo clásico de redes de Petri con características que nos permitan hablar de términos propios de los sistemas ubicuos, como pueden ser componentes, localidad, movilidad, comunicación, coordinación o seguridad. Presentaremos progresivamente distintos modelos que vayan incorporando nuevas características, comparando las distintas extensiones entre sí fundamentalmente a través del estudio de las propiedades de alcanzabilidad, recubrimiento y acotación. Por su especial relevancia desde el punto de vista teórico