Juan Carlos Espinosa Ceniceros: [VVS] 8. Verificación formal de sistemas

Una Red de Petri es un modelo gráfico, formal y abstracto para describir y analizar el flujo de información, sirven como una herramienta matemática para modelar concurrencia, no deterninismo, comunicación y sincronización.

El análisis de las Redes de Petri ayuda a mostrar información importante sobre la estructura y el comportamiento dinámico de los sistemas modelados.

http://astreo.ii.uam.es/~jlara/doctorado.2006/tema7.pdf

Las redes de petri fueron inventadas por el alemán Karl Adam Petri en 1962. En su tesis doctoral "kommunikation mit automaten" (Comunicación con autómatas) establece los fundamentos para el desarrollo teórico de los conceptos básicos de las redes de petri.

Las redes petri son consideradas una herramienta para el estudio de los sistemas, con una red de petri se puede modelar el comportamiento y la estructura de un sistema. Posteriormente se puede analizar el flujo del proceso que el sistema realiza para obtener un resultado, asi como obtener información sobre el comportamiento dinámico del sistema.

Las redes de petri se componen de dos cosas:

Lugares: que permiten representar los estados del sistema mediante la utilización de marcas.
Transiciones: que representan el conjunto de acciones a realizar cuando se cumplen unas determinadas precondiciones en el sistema.

Más ampliamente, una red de Petri es un conjunto formado por la tupla R = {P, T, Pre, Post}, la tupla contiene los componentes básicos que forman su estructura:

Un conjunto de plazas P
Un conjunto de transiciones T
La función de entrada I
La función de salida O

Las funciones de entrada y salida relacionan las transiciones y las plazas.

La función de entrada I es un mapeo a partir del conjunto de plazas de entrada hacia la transición tj, la función se puede escribir como I(tj).

La función de salida O es un mapeo a partir de la transición tj hacia el conjunto de plazas de salida, la función de salida se puede escribir como O(tj).

Ejemplo de Red de Petri: http://www.uhu.es/diego.lopez/AI/auto_trans-tema3.PDF

Hay una serie de condiciones que deben cumplirse en la construcción de las Redes de Petri:

Un arco une siempre lugares con transiciones y nunca dos lugares o dos transiciones.
Una transición puede ser destino de varios lugares y un lugar puede ser el destino devarias transiciones.
Una transición puede ser origen de varios lugares y un lugar puede ser origen de varias transiciones.
Los lugares pueden presentar marcas (una marca se representa mediante un punto en el interior del círculo).
Cada lugar tiene asociada una acción o salida. Los lugares que contiene marcas se consideran lugares activos. Cuando un lugar está activo sus salidas están a uno.
A las transiciones se les asocia eventos (funciones lógicas de las variables de entrada). Una transición se dice que está sensibilizada cuando todos su lugares origen están marcados.
Cuando ocurre un evento asociado a una transición (la función lógica se hace uno), se dice que la transición está validada.

Algunas de las aplicaciones de las Redes de Petri pueden ser diseñar, analizar y diagnosticar:

Sistemas concurrentes
Arquitetura de Computadores
Protocolos de Redes
Sistemas Operativos
Sistemas de Producción
Sistemas Digitales
Hardware/Software
Sistemas de Tiempo Real
Control de Tráfico

Mas información, consultar referencias.

Actividad

La actividad de esta semana consistió en:

Investigar un poco sobre Redes Petri
Inventar un pequeño sistema concurrente
Modelar la Red Petri en Python, utilizando python-snakes

El sistema concurrente que elegí se me ocurrio viendo una maquina de café en el trabajo, asi que comencé a diseñar una red de petri de acuerdo a cómo pienso que funciona esa máquina.

Primero, ¿qué hace la máquina? Básicamente tiene 2 botones, agua o café, y dependiendo de cuál botón presiones dispensará agua caliente o una infusión de café.

Para ello note el siguiente flujo de trabajo:

La máquina está en espera
Presionas el boton de agua caliente o café.
Si eliges café, la maquina toma un poco de café, lo muele y lo coloca en el filtro
La máquina comienza a hacer fluir el agua caliente por el filtro
La máquina dispensa la infusión de café.
La máquina limpia el filtro y espera nuevamente.
Si eliges agua caliente la máquina se brinca los pasos de tomar, moler y colocar el café, solamente hace fluir el agua caliente y vuelve a esperar.

Ahora, hay 2 transiciones que suceden en silencio.

Verificar si hay café en el contenedor, si no, enciende un led rojo como aviso.
Verificar si hay agua en el contenedor, si no, enciende un led rojo (diferente) como aviso.

Entonces, identifiqué los siguientes estados y transiciones:

Estados	Transiciones
Esperando Agua seleccionada Café seleccionado Si hay café Si hay agua Bebida servida No hay café No hay agua	Selecciona bebida Verificar café Verificar agua Servir bebida Limpiar filtro Aviso error