Sistema Maude

El sistema Maude es una implementación de lógica de reescritura . Su enfoque general es similar a la implementación de lógica ecuacional de Joseph Goguen en OBJ3 , pero se basa en lógica de reescritura en lugar de lógica ecuacional ordenada , y hace especial hincapié en una potente metaprogramación basada en la reflexión .

Maude es software libre y hay tutoriales disponibles en línea. Fue desarrollado originalmente en SRI International , ^{[ 1 ]} pero ahora es desarrollado por una colaboración diversa de investigadores. ^{[ 2 ]}

Maude se propone resolver un conjunto de problemas diferente al de los lenguajes imperativos comunes como C , Java o Perl . Es una herramienta de razonamiento formal que nos ayuda a verificar que las cosas son "como deberían" y a mostrarnos por qué no lo son si este es el caso. En otras palabras, Maude nos permite definir formalmente lo que entendemos por un concepto de manera muy abstracta (sin preocuparnos por cómo se representa internamente la estructura, etc.), pero podemos describir lo que se considera equivalente en nuestra teoría ( ecuaciones ) y los cambios de estado por los que puede pasar ( reglas de reescritura ).

Los módulos de Maude (teorías de reescritura) constan de un lenguaje de términos, conjuntos de ecuaciones y reglas de reescritura. Los términos en una teoría de reescritura se construyen mediante operadores (funciones que aceptan cero o más argumentos de algún tipo y que devuelven un término de un tipo específico). Los operadores que no aceptan argumentos se consideran constantes, y el lenguaje de términos se construye mediante estas construcciones simples. Maude permite al usuario especificar si los operadores son infijos, postfijos o prefijos (por defecto); esto se hace utilizando guiones bajos como relleno para los términos de entrada.

Se supone que las ecuaciones de reducción son confluentes y terminantes . Las reglas de reescritura no tienen esta restricción.

Cuando Maude se ejecuta, reescribe los términos según las ecuaciones y las reglas de reescritura. Maude reescribe los términos según las ecuaciones siempre que haya una coincidencia entre los términos cerrados que se intentan reescribir (o reducir) y el lado izquierdo de una ecuación en nuestro conjunto de ecuaciones. Una coincidencia en este contexto es una sustitución de las variables en el lado izquierdo de una ecuación que la deja idéntica al término que se intenta reescribir/reducir. Las ecuaciones y las reglas de reescritura también pueden ser reglas condicionales , lo que significa que deben cumplir ciertos criterios para aplicarse al término (además de simplemente coincidir con el lado izquierdo de la regla de reescritura).

El sistema Maude aplica las reglas de forma aleatoria, lo que significa que no se puede garantizar que una regla se aplique antes que otra, y así sucesivamente. Si se puede aplicar una ecuación al término, siempre se aplicará antes que cualquier regla de reescritura. La búsqueda integrada de Maude puede detectar estados no deseados y demostrar que no se puede alcanzar ninguno. Gracias a la propiedad reflexiva o la lógica de reescritura, Maude tiene la capacidad de controlar qué aplicaciones de reglas se deben intentar en cada paso mediante metaprogramación .

Maude se ha utilizado para validar protocolos de seguridad y código crítico. El sistema Maude ha demostrado fallos en protocolos criptográficos simplemente especificando lo que el sistema puede hacer y buscando situaciones no deseadas (estados o términos que no deberían ser posibles). De esta forma, se puede demostrar que el protocolo contiene errores, no errores de programación, sino situaciones que ocurren y que son difíciles de predecir simplemente siguiendo el camino habitual, como hacen la mayoría de los desarrolladores.

RTX Corporation (anteriormente Raytheon Technologies) utilizó Maude para escribir “una de las primeras herramientas generalizadas y modulares para experimentar con el diseño de sistemas de comunicación ocultos (HCS) a escalas prácticas”. ^{[ 3 ]}

• Clavel, Durán, Eker, Lincoln, Martí-Oliet, Meseguer y Quesada, 1998. Maude como metalenguaje , en Proc. 2nd International Workshop on Rewriting Logic and its Applications, Electronic Notes in Theoretical Computer Science 15, Elsevier.
• Martí-Oliet y José Meseguer , 2002. Reescritura de la lógica: hoja de ruta y bibliografía . Theoretical Computer Science 285(2):121-154.
• Martí-Oliet y José Meseguer , 1993-2000. Reescritura de la lógica como marco lógico y semántico . Electronic Notes in Theoretical Computer Science 4, Elsevier.
• Clavel, Durán, Eker, Lincoln, Martí-Oliet, Meseguer y Talcott (2007). Todo sobre Maude: un marco lógico de alto rendimiento: cómo especificar, programar y verificar sistemas en lógica de reescritura (PDF) . Springer. ISBN 978-3-540-71940-3.{{cite book}}: CS1 maint: varios nombres: lista de autores ( enlace )

• Página principal de Maude en la Universidad de Illinois en Urbana-Champaign;
• La página principal de la herramienta Maude en tiempo real fue archivada el 14 de mayo de 2011 en la Wayback Machine y fue desarrollada por Peter Csaba Ölveczky.
• Introducción a Maude por Neal Harman, Universidad de Swansea ( erratas )
• Arquitectura distribuida basada en políticas y objetivos , escrita en Maude por SRI International.
• Maude para Windows , el instalador de Maude para Windows, y Maude Development Tools , el complemento de Maude para Eclipse desarrollado por el proyecto MOMENT en la Universidad Politécnica de Valencia (España).