Alloy Analyzer
Der Alloy Analyzer ist ein in der Informatik und Softwaretechnik eingesetztes Programm, das dazu genutzt werden kann, um Spezifikationen, die in der Sprache Alloy geschrieben sind, zu analysieren und zu simulieren.[1] Das Programm kann Modelle der Spezifikation (Modelle im Sinne der formalen Logik) erzeugen, also Instanzen aller Invarianten, die in der Spezifikation definiert wurden. Die Sprache Alloy basiert auf relationaler Logik und eignet sich besonders gut dafür, Strukturen zu spezifizieren, wie sie oft im Softwareentwurf auftreten, also zum Beispiel Architekturen, Datenbankschemata, Netzwerk-Topologien, Ontologien u. ä.
| Alloy Analyser | |
|---|---|
 Screenshots mit Beispiel | |
| Basisdaten | |
| Hauptentwickler | Daniel Jackson |
| Aktuelle Version | 6.0.0 (4. November 2021) |
| Betriebssystem | plattformunabhängig |
| Programmiersprache | Java |
| Lizenz | MIT-Lizenz |
| deutschsprachig | nein |
| AlloyTools | |
Darüber hinaus ist es in Alloy möglich, die Dimension Zeit in die Spezifikation einzubeziehen: seit Version 6 kann man in der Sprache unterscheiden zwischen Objekten, die statisch sind, sich also im Laufe der Zeit nicht ändern und solchen, die dynamisch sind, deren Struktur sich von Zeitpunkt zu Zeitpunkt unterscheiden kann. Der Alloy Analyzer zeigt dann nicht nur möglichen statische Strukturen an, die der Spezifikation entsprechen, sondern auch mögliche zeitliche Verläufe, die sich aus ihr ergeben. Für die Formulierung von temporalen Bedingungen stehen in Alloy 6 die Operatoren der linearen temporalen Logik zur Verfügung[2].
Der Alloy Analyzer unterstützt die inkrementelle Entwicklung von Spezifikationen solcher Strukturen, indem er Modelle erzeugt, an denen man überprüfen kann, ob die gewünschten Eigenschaften der Strukturen auch tatsächlich erfüllt werden. Er ist auf diese Weise ein Werkzeug der agilen Modellierung.
Die Sprache Alloy und der Alloy Analyzer werden seit 1997 unter der Leitung von Daniel Jackson am Massachusetts Institute of Technology in den USA entwickelt. Die Bezeichnung „Alloy“ (Deutsch: Legierung) rührt daher, dass Alloy von Konzepten der Spezifikationssprache Z und des Model Checkings beeinflusst wurde.
Analyseansatz
Die Sprache Alloy hat die Ausdrucksmächtigkeit der Prädikatenlogik erster Stufe erweitert um den transitiven Abschluss. Sie ist also nicht entscheidbar. Deshalb wird für die Analyse von Spezifikationen im Alloy Analyzer eine endliche Größe des zu betrachtenden Universums vorgegeben. Dies hat zur Folge, dass die Allgemeingültigkeit der Ergebnisse eingeschränkt ist. Jedoch begründen die Entwickler von Alloy Analyzer die Entscheidung zur Einschränkung des Gültigkeitsbereichs unter Berufung auf die small scope hypothesis[1], die besagt, dass ein hoher Anteil an Programmfehlern bereits gefunden werden kann, wenn man das Programm für alle Eingabewerte eines kleinen Gültigkeitsbereichs prüft.[3]
Durch die Beschränkung auf endliche Universen kann eine Spezifikation in Alloy in eine Formel der Aussagenlogik transformiert werden. Für das Finden von Modellen für die Spezifikation müssen dann Belegungen dieser Formel gefunden werden. Das heißt, die Aufgabe des Alloy Analyzers kann auf das Erfüllbarkeitsproblem der Aussagenlogik zurückgeführt werden.[1] Programme, die das Erfüllbarkeitsproblem lösen, werden SAT Solver genannt. Im Alloy Analyzer wird der Constraint solver Kodkod verwendet, der die Spezifikation in Alloy in die Aussagenlogik transformiert und dann einen SAT-Solver wie z. B. SAT4J verwendet, um erfüllende Belegungen zu finden. Diese werden dann zurücktransformiert in Alloy.
In Alloy 6 können Eigenschaften für die generierten Modell und Ausführungspfade auch verifiziert werden. Dazu kann man sich auf eine endliche Zahl von möglichen Ausführungsschritten beschränken, also bounded model checking durchführen. Es gibt aber auch die Möglichkeit, die Verifikation für beliebig viele Ausführungsschritte zu machen. In diesem Fall wird symbolisches Model Checking mit SMV eingesetzt. Der Alloy Analyzer in Alloy 6 verwendet dazu die Komponente Pardinus, eine Erweiterung von Kodkod, die bounded model checking mit SAT-Solvern unterstützt, aber auch die Model Checker NuSMV oder nuXmv als Backend für unbounded model checking anbinden kann.
Anwendungen
Alloy und der Alloy Analyzer wurden in einem breiten Spektrum von Untersuchungen eingesetzt. Beispiele sind:
- Kritische Systeme, wie etwa in der Medizintechnik.[4]
- Netzwerk-Protokolle: Pamela Zave konnte mit Hilfe des Alloy Analyzers Fehler in Chord finden und Korrekturen vorschlagen.[5]
- Web-Sicherheit: Eine Gruppe an den Universitäten UC Berkeley und Stanford verwendeten Alloy und den Alloy Analyzer um verschiedene Aspekte der Sicherheit im Web zu untersuchen.[6]
- Code-Verifikation: Greg Dennis hat ein Werkzeug namens Forge entwickelt, das Alloy verwendet und Java-Code, der mit Spezifikationen der Java Modeling Language JML annotiert ist überprüfen kann. Dieses Werkzeug wurde zur Verifikation von Java-Bibliotheken[7] sowie von Code eines elektronischen Wahlsystems[8] eingesetzt.
Beispiele
Eine Uhr (nur mit Stundenanzeige) in Alloy 6
one sig Uhr {var stunde: one Int}pred init {Uhr.stunde = 1}pred move {Uhr.stunde = 12 implies Uhr.stunde' = 1 else Uhr.stunde' = Uhr.stunde.plus[1]}fact trans {initalways move}run {} for 5 int, 12 stepsAuswahl eines ausgezeichneten Knotens in einem Ring von Prozessen, siehe Julien Brunel, David Chemouil, Alcino Cunha, Nuno Macedo: Formal Software Design with Alloy 6.[9]
open util/ordering[Node]sig Node { succ : one Node, var inbox : set Node}fact { some Node // at least one node all n : Node | Node in n.^succ // succ forms a ring no inbox // initially inbox is empty}fun Elected : set Node { { n : Node | n not in n.inbox and once (n in n.inbox) }}pred initiate[n : Node] { // node n initiates the protocol historically n not in n.succ.inbox // guard n.succ.inbox' = n.succ.inbox + n // effect on n.succ.inbox all m : Node - n.succ | m.inbox' = m.inbox // effect on the inboxes of other nodes}pred process[n : Node, i : Node] { // i is read and processed by node n i in n.inbox // guard n.inbox' = n.inbox - i // effect on n.inbox gt[i,n] implies n.succ.inbox' = n.succ.inbox + i // effect on n.succ.inbox else n.succ.inbox' = n.succ.inbox all m : Node - n.succ - n | m.inbox' = m.inbox // effect on the inboxes of other nodes}pred stutter { inbox' = inbox}fact { // possible events always ( stutter or some n : Node | initiate[n] or some n : Node, i : Node | process[n,i] )}run example { eventually some Elected} for 3 Nodeassert AtMostOneLeader { always (lone Elected)}check AtMostOneLeader for 5 but 1.. stepspred fairness { all n : Node, i : Node { (eventually always historically n not in n.succ.inbox) implies (always eventually initiate[n]) (eventually always i in n.inbox) implies (always eventually process[n,i]) }}assert AtLeastOneLeader { fairness implies eventually (some Elected)}check AtLeastOneLeader for 3 but 1.. steps