Hasta ahora hemos hablado de la comunicación asíncrona entre procesos a través de canales de mensajes que se declaran, por ejemplo, como
donde N es una constante positiva que define la cantidad máxima de mensajes que se pueden almacenar en el canal. Una…
Los canales de mensajes se usan para modelar el intercambio de datos entre procesos. Se declaran local o globalmente. En la declaración
el typename chan introduce una declaración de canal. En este caso, el canal se llama qname y se declara que es capaz de…
Normalmente, la ejecución del proceso solo se guía por las reglas de sincronización capturadas en la semántica de las declaraciones de las especificaciones de proctype. Sin embargo, es posible definir restricciones globales adicionales en las ejecuciones de procesos. Esto se…
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…
El método que se usa para verificar la correctitud de los diseños de software es estándar en la mayoría de las disciplinas de ingeniería. Este es conocido como Model Checking. Cuando el software en sí mismo no se puede verificar exhaustivamente, podemos construir un modelo…
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…
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…
Hasta el momento, no hemos mostrado ningún ejemplo del uso del envío de mensajes entre procesos asincrónicos. Vamos a…