Maude

Um Protokolle zu testen. Du definierst den Zustand deines Netzwerks als Term. Du definierst Nachrichten als Regeln. msg(A, B) die-on-network -> null (Paketverlust). Maude kann dann alle möglichen Zustände durchsuchen ("Search command") und sagen: "Gibt es einen Zustand, wo beide Deadlock haben?"

1. Reflection

Maude ist reflektiv. Man kann Maude-Regeln in Maude darstellen. Das erlaubt "Meta-Programmierung" auf einem ganz neuen Level. Man kann ganze Strategien ("Erst Innermost, dann Round-Robin") in Maude selbst schreiben.

2. AC-Matching

Maude hat eingebautes Matching für Assoziativität und Kommutativität (AC). Wenn du sagst op _+_ : Nat Nat -> Nat [assoc comm]. Dann matcht die Regel x + x -> 2*x automatisch auch auf a + b + a (weil es a + a + b ist). Das effizient zu implementieren ist ein Meisterwerk der Ingenieurskunst.

1. Rewriting Logic vs. Hoare Logic

Während klassische Verifikation (Hoare Logic) Programme durch Vor- und Nachbedingungen beschreibt, nutzt Maude Rewriting Logic. Ein Zustand ist ein mathematischer Term (z. B. eine Menge von Ressourcen). Eine Aktion ist eine Rewrite Rule. Der große Vorteil: Rewriting Logic ist von Natur aus nebenläufig (concurrent) und nicht-deterministisch. Wenn zwei Regeln auf unterschiedlichen Teilen eines Terms arbeiten können, passiert das in Maude "gleichzeitig". Dies macht es zur perfekten Sprache, um Quanten-Algorithmen, biologische Zellen oder verteilte Datenbanken (wie Cassandra) formal zu modellieren, bei denen viele Dinge gleichzeitig passieren.

2. Narrowing & Symbolic Execution

Maude kann nicht nur Terme ersetzen, sondern auch Narrowing betreiben. Statt einen fixen Term 3 + 2 zu berechnen, kann man Maude fragen: x + 2 -> 5. Was ist x? Maude nutzt Unifikation, um die Platzhalter zu finden. Das ist im Grunde Symbolic Execution. In der Produktion (z.B. bei der Suche nach Sicherheitslücken in Protokollen) erlaubt dies Maude, nicht nur nach bekannten Fehlern zu suchen, sondern ganze Klassen von Angriffsszenarien zu generieren, indem es "symbolische Angreifer" simuliert, die beliebige Nachrichten schicken können.

3. Object-Oriented Maude (Full Maude)

Maude hat eine Erweiterung namens Full Maude, die objektorientierte Konzepte nativ in Rewriting Logic abbildet. Ein "Objekt" ist ein Term der Form < Id : Class | Attr1 : Val1, ... >. Ein "Nachrichtenaustausch" ist eine Rewrite Rule, die zwei Objekte und eine Message konsumiert und neue Zustände erzeugt. Dieses System ist so performant, dass man damit komplexe Cloud-Architekturen simulieren kann, um Durchsatz-Engpässe zu finden, bevor die erste Zeile Java-Code geschrieben wird. Das K-Framework nutzt diese Mächtigkeit, um die Semantik der EVM (Ethereum Virtual Machine) zu definieren und Smart Contracts im Wert von Milliarden Dollar mathematisch abzusichern.