Principios

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…

2.13 Gráfico de programa (PG)

Un gráfico de programa(PG) sobre conjunto Var de variables escritas es una tupla

donde:

La notación

es usada como abreviatura de

2.2 Paralelismo y Comunicación (Parte 3)

En el post previo vimos que podíamos modelar concurrencia de procesos independiente, usando el operador de entrelazado ||| . Sin embargo es demasiado simple como para modelar sistemas paralelos.

Comunicación vía Variables…

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…

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.2 Paralelismo y Comunicación (Parte 2)

Ahora veremos un ejemplo de un sistema de semáforos en paralelo. Asumiremos que cada…

2. Modelando Sistemas Concurrentes

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

2.2 Paralelismo y Comunicación (Parte 1)

En previos posts se introdujo la noción de sistemas de transición y también se mostro como circuitos y pequeños programas podían ser modelados por sistemas de transición. Sin embargo, la mayoría de hardware y software no son secuenciales son secuenciales, si…