Alloy Analyzer

Alloy Analyser
Screenshots mit Beispiel
Basisdaten
Maintainer	Daniel Jackson
Aktuelle Version	4.1.10 (19. März 2009)
Betriebssystem	plattformunabhängig
Programmier­sprache	Java
Lizenz	MIT-Lizenz
Deutschsprachig	nein
alloy.mit.edu

Der Alloy Analyzer ist ein in der Informatik und Softwaretechnik eingesetztes Programm, das dazu genutzt werden kann, um Spezifikationen, die in der gleichnamigen Sprache geschrieben sind, zu analysieren.^[1] Das Analyseprogramm kann Instanzen der Modelinvarianten erzeugen, die Ausführung von Operationen simulieren, die als Teil des Models definiert wurden, und benutzerdefinierte Eigenschaften des Models überprüfen. Es unterstützt auch die Analyse von Teilmodellen, ebenso die inkrementelle Analyse von Modellen, so wie sie erstellt werden, und Rückgabe direkter Ergebnisse an den Anwender.

Das Analyseprogramm und die zugehörige Alloy-Sprache wurden unter Leitung von Daniel Jackson am Massachusetts Institute of Technology in den USA entwickelt. Der erste Prototyp wurde bereits 1997 entwickelt.

Analyseansatz

Der Alloy Analyser wurde insbesondere entwickelt für sogenannte leichte Formale Methoden ("lightweight formal methods"). Beispielsweise ist es beabsichtigt vollständige, automatische Analyse zu unterstützen, im Gegensatz zu interaktiven Theorembeweistechniken, die im Allgemeinen von ähnlichen Sprachen wie Alloy benutzt werden. Die Entwicklung von Alloy wurde beeinflusst von der automatischen Analyse, die von Model Checkern angeboten wird. Jedoch ist Model Checking ungeeignet für die Art von Modellen, die mit Alloy entwickelt werden. Demnach wurde der Kern der Anwendung letztlich als Model-finder auf einem SAT-Solver aufgebaut.^[1]

In Version 3.0 umschloss der Alloy Analyser einen eingebauten SAT-basierten Model-finder, der auf einem Standardsolver beruht. Mit der Version 4.0 wurde allerdings der Kodkod Model-finder integriert, für den der Alloy Analyser als Front-End dient. Beide Model-finder übersetzen hauptsächlich ein Model von Relationaler Logik in eine entsprechende Formel der Booleschen Algebra und berufen sich dann auf einen Standard-SAT-Solver. In Falle, dass der Solver eine Lösung findet, wird das Ergebnis zurück in die entsprechende Bindung von Konstanten zu Variablen im Relationalen Model transformiert.^[2]

Um sicherzustellen, dass das Problem der Modellsuche entscheidbar ist, führt der Alloy Analyzer eine Modellsuche über einem beschränktem Gültigkeitsbereich bestehend aus einer endlichen Anzahl benutzerdefinierten Objekte aus. 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]

Einzelnachweise

1. ↑ ^{a b c} Daniel Jackson: Software Abstrations: Logic, Language, and Analysis. MIT Press, 2006, ISBN 978-0-262-10114-1.
2. ↑ Torlak, E.; G. Dennis (April 2008). "Kodkod for Alloy Users" (PDF). First ACM Alloy Workshop. Portland, Oregon, Aufgerufen am 24. Dezember 2009
3. ↑ Alexandr Andoni, Dumitru Daniliuc, Sarfraz Khurshid und Darko Marinov (2002), "Evaluating the small scope hypothesis"

Weblinks

• Alloy Community Website am MIT
• Eine Anleitung für Alloy
• Kodkod Model-finder am MIT