3. Una visión general de PROMELA

Los modelos PROMELA se basan en los aspectos de coordinación y sincronización de un sistema distribuido, y no en sus aspectos computacionales. Hay algunas buenas razones para esta elección. En primer lugar, el diseño y la verificación de las estructuras de coordinación…

Construyendo Modelos de Verificación con SPIN Model Checker

Para verificar un sistema, necesitamos describir dos cosas: el conjunto de hechos que queremos verificar y los aspectos relevantes del sistema que se necesitan para verificar esos hechos. Comenzaremos con una introducción al…

2.6 Exclusión mutua

Quizás el mejor ejemplo de la dificultad de diseñar esquemas de coordinación correctos para ejecutar procesos de forma…

Ejemplo 2.5. Algoritmo de exclusión mutua de Peterson (1981)

Gran parte del algoritmo parece familiar, aparte de la maravillosa simplicidad de la solución. Ahora podemos preguntarnos de nuevo, ¿no…

2. Modelando Sistemas Concurrentes

Un pre-requisito para la verificación de modelos(model checking) es un modelo del sistema bajo…

Encontrando errores en sistemas concurrentes

El SPIN model checker, puede verificar la correctitud de un sistema concurrente, para lo cual se necesita de un modelo que refeje los elementos esenciales del sistema. En caso de no satisfacer los requerimientos, se puede producir un ejemplo para…

2.1.1 Ejecuciones de un sistema de transición

El comportamiento de sistema de transición ha sido descrito en un nivel intuitivo. Ahora formalizaremos usando la noción de ejecuciones(execution).

Una ejecución describe el posible comportamiento del sistema de transición.

2.1.2 Modelado de sistemas de hardware y software

Esta sección ilustra el uso de sistemas de transición mediante la elaboración de modelos de circuitos de hardware (síncronos) y sistemas secuenciales dependientes de datos, una especie de programas informáticos. Para ambos casos, el concepto…

Aumento de la usabilidad de la verificación de código C basada en spin utilizando un lenguaje de definición de arnés

2.1.2 Sistemas dependientes de datos (Parte 2)

Las acciones ejecutables de un sistema dependiente de datos normalmente resultan de una bifurcación condicional, como en

En principio, cuando se modela este fragmento de programa como un sistema de transición, las…