PROMELA ( Process or Protocol Meta Language ) es un lenguaje de modelado de verificación introducido por Gerard J. Holzmann . El lenguaje permite la creación dinámica de procesos concurrentes para modelar, por ejemplo, sistemas distribuidos . En los modelos PROMELA, la comunicación a través de canales de mensajes se puede definir como sincrónica (es decir, de encuentro) o asincrónica (es decir, con buffer). Los modelos PROMELA se pueden analizar con el verificador de modelos SPIN , para verificar que el sistema modelado produce el comportamiento deseado. También está disponible una implementación verificada con Isabelle/HOL , como parte del proyecto Computer Aided Verification of Automata (CAVA). [1] [2] Los archivos escritos en Promela tradicionalmente tienen una extensión de archivo ..pml
PROMELA es un lenguaje de modelado de procesos cuyo uso previsto es verificar la lógica de sistemas paralelos. Dado un programa en PROMELA, Spin puede verificar la corrección del modelo realizando simulaciones aleatorias o iterativas de la ejecución del sistema modelado, o puede generar un programa en C que realice una verificación rápida y exhaustiva del espacio de estados del sistema. Durante las simulaciones y verificaciones, SPIN verifica la ausencia de bloqueos, recepciones no especificadas y código no ejecutable. El verificador también se puede utilizar para demostrar la corrección de las invariantes del sistema y puede encontrar ciclos de ejecución sin progreso. Finalmente, admite la verificación de restricciones temporales de tiempo lineal; ya sea con Promela never-claims o formulando directamente las restricciones en lógica temporal . Cada modelo se puede verificar con SPIN bajo diferentes tipos de suposiciones sobre el entorno. Una vez que se ha establecido la corrección de un modelo con SPIN, ese hecho se puede utilizar en la construcción y verificación de todos los modelos posteriores.
Los programas PROMELA constan de procesos, canales de mensajes y variables . Los procesos son objetos globales que representan las entidades concurrentes del sistema distribuido. Los canales de mensajes y las variables se pueden declarar de forma global o local dentro de un proceso. Los procesos especifican el comportamiento, los canales y las variables globales definen el entorno en el que se ejecutan los procesos.
Los tipos de datos básicos utilizados en PROMELA se presentan en la siguiente tabla. Los tamaños en bits corresponden a una computadora PC i386/Linux.
Los nombres bit y bool son sinónimos de un único bit de información. Un byte es una cantidad sin signo que puede almacenar un valor entre 0 y 255. Los short y los int son cantidades con signo que difieren solo en el rango de valores que pueden contener.
Las variables también se pueden declarar como matrices. Por ejemplo, la declaración:
int x [ 10 ]; declara una matriz de 10 números enteros a los que se puede acceder en expresiones de subíndice de matriz como:
x[0] = x[1] + x[2];
Pero las matrices no se pueden enumerar al crearlas, por lo que deben inicializarse de la siguiente manera:
int x [ 3 ]; x [ 0 ] = 1 ; x [ 1 ] = 2 ; x [ 2 ] = 3 ; El índice de una matriz puede ser cualquier expresión que determine un valor entero único. El efecto de un índice fuera del rango no está definido. Las matrices multidimensionales se pueden definir indirectamente con la ayuda de la construcción typedef (ver a continuación).
El estado de una variable o de un canal de mensajes solo puede ser modificado o inspeccionado por procesos. El comportamiento de un proceso se define mediante una declaración de tipo de proceso . Por ejemplo, lo siguiente declara un proceso de tipo A con un estado de variable:
tipo de procedimiento A() { estado del byte; estado = 3; }La definición de proctype solo declara el comportamiento del proceso, no lo ejecuta. Inicialmente, en el modelo PROMELA, se ejecutará un solo proceso: un proceso de tipo init , que debe declararse explícitamente en cada especificación PROMELA.
Se pueden generar nuevos procesos utilizando la sentencia run , que toma un argumento que consiste en el nombre de un proctype , a partir del cual se crea una instancia de un proceso. El operador run se puede utilizar en el cuerpo de las definiciones de proctype , no solo en el proceso inicial. Esto permite la creación dinámica de procesos en PROMELA.
Un proceso en ejecución desaparece cuando finaliza, es decir, cuando llega al final del cuerpo en la definición de proctype y todos los procesos secundarios que inició han finalizado.
Un proctipo también puede estar activo (abajo).
Al anteponer la palabra clave atomic a una secuencia de instrucciones entre llaves , el usuario puede indicar que la secuencia se ejecutará como una unidad indivisible, no intercalada con ningún otro proceso.
atómico { declaraciones; }Las secuencias atómicas pueden ser una herramienta importante para reducir la complejidad de los modelos de verificación. Tenga en cuenta que las secuencias atómicas restringen la cantidad de intercalación que se permite en un sistema distribuido. Los modelos intratables pueden volverse manejables etiquetando todas las manipulaciones de las variables locales con secuencias atómicas.
Los canales de mensajes se utilizan para modelar la transferencia de datos de un proceso a otro. Se declaran local o globalmente, por ejemplo, de la siguiente manera:
chan qname = [16] de {corto}Esto declara un canal con buffer que puede almacenar hasta 16 mensajes de tipo corto ( la capacidad es 16 aquí).
La declaración:
nombre_q ! expr;
envía el valor de la expresión expr al canal con nombre qname , es decir, agrega el valor al final del canal.
La declaración:
nombre_de_usuario ? msg;
Recibe el mensaje, lo recupera del encabezado del canal y lo almacena en la variable msg. Los canales pasan los mensajes en orden de entrada-salida.
Un puerto de encuentro se puede declarar como un canal de mensajes con una longitud de almacenamiento de cero. Por ejemplo, lo siguiente:
puerto chan = [0] de {byte}define un puerto de encuentro que puede pasar mensajes de tipo byte . Las interacciones de mensajes a través de dichos puertos de encuentro son, por definición, sincrónicas, es decir, el emisor o receptor (el que llega primero al canal) bloqueará al contendiente que llegue en segundo lugar (receptor o emisor).
Cuando un canal almacenado en búfer se ha llenado hasta su capacidad máxima (el envío es el número de salidas por "capacidad" antes de recibir las entradas), el comportamiento predeterminado del canal es volverse sincrónico y el remitente se bloqueará en el siguiente envío. Observe que no hay un búfer de mensajes común compartido entre canales. En comparación con el uso de un canal unidireccional y punto a punto, es posible compartir canales entre varios receptores o varios remitentes y fusionar flujos de datos independientes en un único canal compartido. De esto se deduce que un único canal también se puede utilizar para la comunicación bidireccional.
En PROMELA existen tres estructuras de control de flujo: la selección de casos , la repetición y el salto incondicional .
La estructura de selección es la más sencilla de construir. Si se utilizan los valores relativos de dos variables a y b , por ejemplo, se puede escribir:
si :: (a != b) -> opción1 :: (a == b) -> opción2 en finLa estructura de selección contiene dos secuencias de ejecución, cada una precedida por dos puntos dobles. Se ejecutará una secuencia de la lista. Una secuencia solo se puede seleccionar si su primera instrucción es ejecutable. La primera instrucción de una secuencia de control se denomina guard .
En el ejemplo anterior, las protecciones son mutuamente excluyentes, pero no necesariamente lo son. Si más de una protección es ejecutable, se selecciona una de las secuencias correspondientes de manera no determinista. Si ninguna de las protecciones es ejecutable, el proceso se bloqueará hasta que se pueda seleccionar una de ellas. (Por el contrario, el lenguaje de programación Occam se detendría o no podría continuar si no hubiera protecciones ejecutables).
si :: (A == verdadero) -> opción1; :: (B == true) -> option2; /* Puede llegar aquí también si A==true */ :: de lo contrario -> opción_fallthrough; en finLa consecuencia de la elección no determinista es que, en el ejemplo anterior, si A es verdadera, se pueden elegir ambas opciones . En la programación "tradicional", se entendería una estructura if – if – else de forma secuencial. Aquí, if – dos puntos – dos puntos debe entenderse como "alguien que esté listo" y si nadie está listo, solo entonces se elegiría else .
si :: valor = 3; :: valor = 4; en finEn el ejemplo anterior, al valor se le asigna de manera no determinista el valor 3 o 4.
Hay dos pseudodeclaraciones que se pueden utilizar como protecciones: la declaración timeout y la declaración else . La declaración timeout modela una condición especial que permite a un proceso interrumpir la espera de una condición que puede que nunca se cumpla. La declaración else se puede utilizar como la declaración inicial de la última secuencia de opciones en una declaración de selección o iteración. La else solo es ejecutable si todas las demás opciones de la misma selección no son ejecutables. Además, la else no se puede utilizar junto con canales.
Una extensión lógica de la estructura de selección es la estructura de repetición. Por ejemplo:
hacer :: contar = contar + 1 :: a = b + 2 :: (cuenta == 0) -> romper sobredosisdescribe una estructura de repetición en PROMELA. Solo se puede seleccionar una opción a la vez. Una vez que se completa la opción, se repite la ejecución de la estructura. La forma normal de finalizar la estructura de repetición es con una instrucción break . Esta transfiere el control a la instrucción que sigue inmediatamente a la estructura de repetición.
Otra forma de romper un bucle es la instrucción goto . Por ejemplo, se puede modificar el ejemplo anterior de la siguiente manera:
hacer :: contar = contar + 1 :: a = b + 2 :: (count == 0) -> ir al final sobredosis hecho: saltar;En este ejemplo, el goto salta a una etiqueta llamada done. Una etiqueta solo puede aparecer antes de una instrucción. Para saltar al final del programa, por ejemplo, resulta útil una instrucción ficticia skip : es un marcador de posición que siempre es ejecutable y no tiene efecto.
Una construcción importante del lenguaje en PROMELA que necesita una pequeña explicación es la declaración assert . Declaraciones de la forma:
afirmar(cualquier_condición_booleana)
siempre son ejecutables. Si se cumple una condición booleana especificada, la instrucción no tiene efecto. Sin embargo, si la condición no se cumple necesariamente, la instrucción producirá un error durante las verificaciones con SPIN .
Una definición de tipo PROMELA se puede utilizar para introducir un nuevo nombre para una lista de objetos de datos de tipos predefinidos o definidos anteriormente. El nuevo nombre de tipo se puede utilizar para declarar e instanciar nuevos objetos de datos, que se pueden utilizar en cualquier contexto de forma obvia:
typedef MyStruct { corto Campo1 ; byte Campo2 ; }; El acceso a los campos declarados en una construcción typedef se realiza de la misma manera que en el lenguaje de programación C. Por ejemplo:
MiEstructura x;x.Campo1 = 1;
es una secuencia PROMELA válida que asigna al campo Campo1 de la variable x el valor 1 .
La palabra clave activa se puede anteponer a cualquier definición de proctype . Si la palabra clave está presente, una instancia de ese proctype estará activa en el estado inicial del sistema. Se pueden especificar múltiples instancias de ese proctype con un sufijo de matriz opcional de la palabra clave. Ejemplo:
proctype activo A() { ... } activo [4] proctype B() { ... }La semántica de ejecutabilidad proporciona los medios básicos en Promela para modelar sincronizaciones de procesos.
tipo_m = {M_ARRIBA, M_DW}; chan Chan_data_down = [0] de {mtype}; chan Chan_data_up = [0] de {mtype}; proctype P1 (chan Chan_datos_de_entrada, Chan_datos_de_salida) { hacer :: Chan_data_in ? M_UP -> saltar; :: Chan_data_out ! M_DW -> saltar; sobredosis; }; proctype P2 (chan Chan_datos_de_entrada, Chan_datos_de_salida) { hacer :: Chan_data_in ? M_DW -> saltar; :: Chan_data_out ! M_UP -> saltar; sobredosis; }; Inicial { atómico { ejecutar P1 (Chan_data_arriba, Chan_data_abajo); ejecutar P2 (Chan_data_down, Chan_data_up); } }En el ejemplo, los dos procesos P1 y P2 tienen opciones no deterministas de (1) entrada del otro o (2) salida al otro. Son posibles dos apretones de manos de encuentro, o ejecutables , y se elige uno de ellos. Esto se repite indefinidamente. Por lo tanto, este modelo no se bloqueará.
Cuando Spin analiza un modelo como el anterior, verificará las opciones con un algoritmo no determinista , donde se explorarán todas las opciones ejecutables. Sin embargo, cuando el simulador de Spin visualiza posibles patrones de comunicación no verificados, puede utilizar un generador aleatorio para resolver la opción "no determinista". Por lo tanto, el simulador puede no mostrar una ejecución incorrecta (en el ejemplo, no hay un rastro incorrecto). Esto ilustra una diferencia entre verificación y simulación. Además, también es posible generar código ejecutable a partir de modelos Promela utilizando Refinement. [3]
Los siguientes identificadores están reservados para su uso como palabras clave.