Murφ

Murφ (/ˈmɝ.fi/, también escrito Murphi ) es un verificador de modelos de estado explícito desarrollado en la Universidad de Stanford y ampliamente utilizado para la verificación formal de protocolos de coherencia de caché.

Historia

La historia temprana de Murφ se describe en un artículo de David Dill. ^{[ 1 ]} La primera versión de Murφ fue diseñada en la Universidad de Stanford en 1990 y 1991 por el Prof. David Dill y sus estudiantes de posgrado Andreas Drexler, Alan Hu y Han Yang, y fue implementada principalmente por Andreas Drexler. El lenguaje de especificación fue ampliamente modificado y extendido por David Dill, Alan Hu, C. Norris Ip, Ralph Melton, Seungjoon Park y Han Yang. Ralph Melton implementó la nueva versión durante el verano y otoño de 1992. Seungjoon Park agregó verificación de vivacidad y restricciones de equidad, pero debido a que el algoritmo para la verificación de vivacidad entraba en conflicto con optimizaciones importantes, particularmente la reducción de simetría, la verificación de vivacidad se omitió en versiones posteriores. C. Norris Ip implementó reglas reversibles y constructores de repetición (que no están incluidos en la versión 3.1), y agregó reducciones de simetría y multiconjuntos (que sí lo están). Ulrich Stern implementó la compactación de hash, ^{[ 2 ]} mejoró el uso del disco e implementó Parallel Murφ.

La última versión publicada por Stanford fue la versión 3.1 en noviembre de 1993. Desde entonces, otros grupos han creado muchas versiones derivadas de Murφ .

Características

El compilador Murφ acepta un modelo escrito en el lenguaje de especificación Murφ y genera código C++ que constituye un verificador para dicho modelo. (Es decir, el código C++, al ejecutarse, realiza una verificación de modelo de estado explícito sobre el diseño descrito por la especificación). El lenguaje de especificación Murφ utiliza comandos protegidos y un modelo de concurrencia asíncrono e intercalado, con toda la sincronización y comunicación realizadas a través de variables globales. El verificador comprueba las propiedades de seguridad en forma de invariantes y aserciones internas especificadas en el modelo, y verifica la presencia de interbloqueos. No comprueba las propiedades de vivacidad, aunque la versión 2.7L de Murφ sí admitía la verificación de un conjunto de propiedades de vivacidad LTL comunes. El lenguaje y el verificador admiten algunos tipos de reducciones de simetría. ^{[ 3 ]}

Murφ se aplicó originalmente para verificar protocolos de coherencia de caché , ^{[ 4 ]} pero también se ha aplicado a otros problemas, incluida la verificación de protocolos de seguridad .

Licencias

La licencia de Murφ es similar a la licencia MIT. Murφ puede usarse, copiarse, modificarse, venderse y redistribuirse para cualquier propósito, siempre que se incluyan el aviso de derechos de autor y la licencia, no se utilice el nombre de la Universidad de Stanford para publicidad sin permiso, y las versiones modificadas no se denominen Murphi sin autorización.

Derivados

Se han creado muchas versiones derivadas de Murφ, tanto en Stanford como en otros lugares, incluidas las siguientes:

Murφ paralelo
Eddy — Murφ paralelo y distribuido.
PReach (Parallel Reachability): comprobación de modelos en paralelo implementada en Erlang.
Murphi distribuido
Murphi de paseo aleatorio paralelo
PAM — Abstracción de predicados Murphi
POeM — Murphi habilitado para orden parcial
CMurphi — Almacenamiento en caché de Murphi.
FHP-Murphi — Murphi probabilístico de horizonte finito.
Eddy Murphi: Paralelo y distribuido, basado en CMurphi, que utiliza MPI para el paso de mensajes.
Universal Planner Murphi: planificación y planificación universal para modelos PDDL+ continuos, lineales y no lineales, con procesos y eventos; también literales iniciales temporizados y flujos iniciales temporizados.
rumor

Véase también

Referencias

↑ Dill, David L. (2008). Grumberg, Orna; Veith, Helmut (eds.). 25 años de verificación de modelos: historia, logros, perspectivas . págs. 77–88 .
↑ Stern, Ulrich; Dill, David L. (1996). Formal Description Techniques IX . Boston, MA: Springer. pp. 333– 348.
↑ Ip, C. Norris; Dill, David L. (1993). "Verificación eficiente de sistemas concurrentes simétricos". Actas de la Conferencia Internacional IEEE de Diseño de Computadoras de 1993 (ICCD'93) . IEEE. págs. 230–234 . doi : 10.1109/ICCD.1993.393375 . ISBN 0-8186-4230-0. S2CID 38444364 .
↑ Dill, David L.; Drexler, Andreas J.; Hu, Alan J.; Yang, C. Han (1992). "Verificación de protocolos como ayuda para el diseño de hardware". Actas de la Conferencia Internacional IEEE de 1992 sobre Diseño de Computadoras: VLSI en Computadoras y Procesadores . IEEE: 552–525 .

Enlaces externos

Manual de referencia anotado de Murphi, versión 3.1
Laboratorio de Seguridad de Stanford, Métodos de verificación de modelos para protocolos de seguridad
Universidad de Utah, Escuela de Informática: una colección de versiones de Murφ.

[1] Dill, David L. (2008). Grumberg, Orna; Veith, Helmut (eds.). 25 años de verificación de modelos: historia, logros, perspectivas . págs. 77–88 .

[2] Stern, Ulrich; Dill, David L. (1996). Formal Description Techniques IX . Boston, MA: Springer. pp. 333– 348.

[3] Ip, C. Norris; Dill, David L. (1993). "Verificación eficiente de sistemas concurrentes simétricos". Actas de la Conferencia Internacional IEEE de Diseño de Computadoras de 1993 (ICCD'93) . IEEE. págs. 230–234 . doi : 10.1109/ICCD.1993.393375 . ISBN 0-8186-4230-0. S2CID 38444364 .

[4] Dill, David L.; Drexler, Andreas J.; Hu, Alan J.; Yang, C. Han (1992). "Verificación de protocolos como ayuda para el diseño de hardware". Actas de la Conferencia Internacional IEEE de 1992 sobre Diseño de Computadoras: VLSI en Computadoras y Procesadores . IEEE: 552–525 .

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]