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 síncrona (es decir, encuentro) o asíncrona (es decir, con búfer). 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 delProyecto de Verificación Asistida por Computadora de Autómatas . [1] Los archivos escritos en Promela tradicionalmente tienen una .pml
extensión de archivo .
Introducción
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 realiza una verificación rápida y exhaustiva del espacio de estado del sistema. Durante las simulaciones y verificaciones, SPIN comprueba la ausencia de interbloqueos, recepciones no especificadas y código no ejecutable. El verificador también se puede utilizar para probar la exactitud de las invariantes del sistema y puede encontrar ciclos de ejecución que no progresan. Finalmente, apoya la verificación de restricciones temporales de tiempo lineal; ya sea con Promela never-afirma o formulando directamente las limitaciones en la lógica temporal . Cada modelo se puede verificar con Spin bajo diferentes tipos de supuestos sobre el medio ambiente. Una vez que se ha establecido la exactitud de un modelo con Spin, ese hecho se puede utilizar en la construcción y verificación de todos los modelos posteriores.
Los programas de 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 global o localmente 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.
Referencia idiomática
Tipos de datos
Los tipos de datos básicos utilizados en PROMELA se presentan en la siguiente tabla. Los tamaños en bits se dan para una máquina PC i386 / Linux.
Nombre | Tamaño (bits) | Uso | Distancia |
---|---|---|---|
un poco | 1 | no firmado | 0..1 |
bool | 1 | no firmado | 0..1 |
byte | 8 | no firmado | 0..255 |
mtype | 8 | no firmado | 0..255 |
corto | dieciséis | firmado | -2 15 ..2 15 - 1 |
En t | 32 | firmado | –2 31 ..2 31 - 1 |
Los nombres bit
y bool
son sinónimos de una sola información. A byte
es una cantidad sin signo que puede almacenar un valor entre 0 y 255. cortos ys 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 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 en la creación, 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 typedef
construcción (ver más abajo).
Procesos
El estado de una variable o de un canal de mensajes solo puede modificarse o inspeccionarse mediante procesos. El comportamiento de un proceso se define mediante una declaración proctype . Por ejemplo, lo siguiente declara un tipo de proceso A con un estado de variable:
proctype A (){ estado de byte; estado = 3;}
La definición de proctype solo declara el comportamiento del proceso, no lo ejecuta. Inicialmente, en el modelo PROMELA, solo se ejecutará un proceso: un proceso de tipo init , que debe declararse explícitamente en cada especificación PROMELA.
Se pueden generar nuevos procesos utilizando la instrucción 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 de ejecución 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 termina, es decir, cuando llega al final del cuerpo en la definición de proctipo , y todos los procesos secundarios que comenzó han terminado.
Un proctipo también puede estar activo (abajo).
Construcción atómica
Al anteponer una secuencia de declaraciones entre llaves con la palabra clave atomic
, 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 entrelazado que se permite en un sistema distribuido. Los modelos intratables pueden hacerse manejables etiquetando todas las manipulaciones de variables locales con secuencias atómicas.
Paso de mensajes
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 {short}
Esto declara un canal en búfer que puede almacenar hasta 16 mensajes de tipo corto (la capacidad es de 16 aquí).
La declaración:
qname! expr;
envía el valor de la expresión expr al canal con el nombre qname , es decir, agrega el valor al final del canal.
La declaración:
qname? msg;
recibe el mensaje, lo recupera del encabezado del canal y lo almacena en la variable msg. Los canales pasan mensajes en orden de primero en entrar, primero en salir.
Un puerto de encuentro se puede declarar como un canal de mensajes con la longitud de almacenamiento 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, síncronas, es decir, el remitente o el receptor (el que llega primero al canal) se bloqueará para el contendiente que llegue en segundo lugar (receptor o remitente).
Cuando un canal con búfer se ha llenado a su capacidad (el envío es el número de "capacidad" de salidas por delante de las entradas de recepción), el comportamiento predeterminado del canal es volverse síncrono y el remitente se bloqueará en el próximo envío. Observe que no hay un búfer de mensajes común compartido entre canales. Aumentando la complejidad, en comparación con el uso de un canal como unidireccional y punto a punto, es posible compartir canales entre múltiples receptores o múltiples remitentes, y fusionar flujos de datos independientes en un solo canal compartido. De esto se deduce que también se puede utilizar un solo canal para la comunicación bidireccional.
Construcciones de flujo de control
Hay tres construcciones de flujo de control en PROMELA. Son la selección de casos , la repetición y el salto incondicional .
Selección de caso
La construcción más simple es la estructura de selección. El uso de los valores relativos de dos variables a y b , por ejemplo, se puede escribir:
Si:: (a! = b) -> opción1:: (a == b) -> opción2fi
La 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 se puede seleccionar solo si su primera instrucción es ejecutable. La primera declaración de una secuencia de control se llama guardia .
En el ejemplo anterior, los protectores son mutuamente excluyentes, pero no es necesario que lo sean. Si se puede ejecutar más de una guarda, una de las secuencias correspondientes se selecciona de forma no determinista. Si todos los guardias no se pueden ejecutar, el proceso se bloqueará hasta que se pueda seleccionar uno de ellos. (En el lado opuesto, el lenguaje de programación occam se detendría o no podría continuar sin guardias ejecutables).
Si:: (A == verdadero) -> opción1;:: (B == verdadero) -> opción2; / * Puede llegar aquí también si A == verdadero * /:: else -> fallthrough_option;fi
La consecuencia de la elección no determinista es que, en el ejemplo anterior, si A es verdadera, se pueden tomar ambas opciones . En la programación "tradicional", se entendería secuencialmente una estructura if - if - else . En este caso, los dos puntos dobles if (dos puntos) deben entenderse como "cualquiera que esté listo" y, si ninguno está listo, solo entonces se tomará el otro .
Si:: valor = 3;:: valor = 4;fi
En el ejemplo anterior, al valor se le da de forma no determinista el valor 3 o 4.
Hay dos pseudo-sentencias que se pueden usar como guardias: la sentencia de tiempo de espera y la sentencia else . La declaración de tiempo de espera modela una condición especial que permite a un proceso abortar la espera de una condición que puede que nunca se cumpla. La instrucción else se puede utilizar como instrucción inicial de la última secuencia de opciones en una instrucción de selección o iteración. El else solo es ejecutable si todas las demás opciones de la misma selección no son ejecutables. Además, el else no se puede utilizar junto con los canales.
Repetición (bucle)
Una extensión lógica de la estructura de selección es la estructura de repetición. Por ejemplo:
hacer:: cuenta = cuenta + 1:: a = b + 2:: (cuenta == 0) -> descansosobredosis
describe una estructura de repetición en PROMELA. Solo se puede seleccionar una opción a la vez. Una vez completada la opción, se repite la ejecución de la estructura. La forma normal de terminar la estructura de repetición es con una declaración de interrupción . Transfiere el control a la instrucción que sigue inmediatamente a la estructura de repetición.
Saltos incondicionales
Otra forma de romper un bucle es la goto
declaración. Por ejemplo, se puede modificar el ejemplo anterior de la siguiente manera:
hacer:: cuenta = cuenta + 1:: a = b + 2:: (cuenta == 0) -> ir a hechosobredosishecho:saltar;
El goto en este ejemplo salta a una etiqueta llamada done. Una etiqueta solo puede aparecer antes de una declaración. Para saltar al final del programa, por ejemplo, un salto de declaración ficticia es útil: es un marcador de posición que siempre es ejecutable y no tiene ningún efecto.
Afirmaciones
Una importante construcción del lenguaje en PROMELA que necesita una pequeña explicación es la aserción comunicado. Declaraciones del formulario:
afirmar (cualquier_condición_booleana)
son siempre ejecutables. Si se cumple una condición booleana especificada, la declaración no tiene ningún efecto. Sin embargo, si la condición no se cumple necesariamente, la declaración producirá un error durante las verificaciones con Spin .
Estructuras de datos complejas
Se puede utilizar una definición de typedef de PROMELA 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 usar para declarar y crear instancias de nuevos objetos de datos, que se pueden usar en cualquier contexto de una manera obvia:
typedef MyStruct { corta Campo1 ; byte Field2 ; };
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:
MyStruct x;x.Campo1 = 1;
es una secuencia PROMELA válida que asigna al campo Campo1 de la variable x el valor 1 .
Proctipos activos
La active
palabra clave 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 () {...}
Ejecutabilidad
La semántica de ejecutabilidad proporciona los medios básicos en Promela para modelar sincronizaciones de procesos.
mtype = {M_UP, M_DW};chan Chan_data_down = [0] de {mtype};chan Chan_data_up = [0] de {mtype};proctype P1 (chan Chan_data_in, Chan_data_out){ hacer :: Chan_data_in? M_UP -> saltar; :: Chan_data_out! M_DW -> saltar; sobredosis;};proctype P2 (chan Chan_data_in, Chan_data_out){ hacer :: Chan_data_in? M_DW -> saltar; :: Chan_data_out! M_UP -> saltar; sobredosis;};en eso{ atómico { ejecutar P1 (Chan_data_up, Chan_data_down); 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 del otro. Dos apretones de manos de encuentro son posibles, o ejecutables , y se elige uno de ellos. Esto se repite para siempre. 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 usar un generador aleatorio para resolver la elección "no determinista". Por lo tanto, es posible que el simulador no muestre una mala ejecución (en el ejemplo, no hay un seguimiento 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 de Promela utilizando Refinement. [2]
Palabras clave
Los siguientes identificadores están reservados para su uso como palabras clave.
- activo
- afirmar
- atómico
- un poco
- bool
- rotura
- byte
- chan
- d_step
- D_proctype
- hacer
- demás
- vacío
- activado
- fi
- completo
- ir
- oculto
- Si
- en línea
- en eso
- En t
- len
- mtype
- vacío
- Nunca
- completo
- sobredosis
- de
- pc_value
- printf
- prioridad
- prototipo
- previsto
- correr
- corto
- saltar
- se acabó el tiempo
- typedef
- a no ser que
- no firmado
- xr
- xs
Referencias
- ^ https://cava.in.tum.de/templates/publications/promela.pdf
- ^ Sharma, Asankhaya. "Un cálculo de refinamiento para Promela". Ingeniería de Sistemas Computacionales Complejos (ICECCS), 2013 18ª Conferencia Internacional sobre. IEEE, 2013.