Alloy Analyser

Screenshots mit Beispiel
Basisdaten
Maintainer Daniel Jackson
Aktuelle Version 6.0.0
(4. November 2021)
Betriebssystem plattformunabhängig
Programmiersprache Java
Lizenz MIT-Lizenz
deutschsprachig nein
AlloyTools

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. 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. ä.

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.

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, 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.

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. 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.
  • Netzwerk-Protokolle: Pamela Zave konnte mit Hilfe des Alloy Analyzers Fehler in Chord finden und Korrekturen vorschlagen.
  • 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.
  • 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 sowie von Code eines elektronischen Wahlsystems 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 {
	init
	always move
}

run {} for 5 int, 12 steps

Auswahl eines ausgezeichneten Knotens in einem Ring von Prozessen, siehe Julien Brunel, David Chemouil, Alcino Cunha, Nuno Macedo: Formal Software Design with Alloy 6.

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 Node

assert AtMostOneLeader {
  always (lone Elected)
}
check AtMostOneLeader for 5 but 1.. steps

pred 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

Einzelnachweise

  1. 1 2 3 Daniel Jackson: Software Abstrations: Logic, Language, and Analysis. MIT Press, 2012, ISBN 978-0-262-01715-2.
  2. ↑ Diese Erweiterung von Alloy wurde zunächst unter dem Namen Electrum entwickelt von Julien Brunel, David Chemouil, Alcino Cunha und Nuno Macedo; siehe Julien Brunel u. a. „The electrum analyzer: model checking relational first- order temporal specifications“. In: Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, September 3-7, 2018. Hrsg. von Marianne Huchard, Christian Kästner und Gordon Fraser. ACM, 2018, S. 884–887.
  3. ↑ Alexandr Andoni, Dumitru Daniliuc, Sarfraz Khurshid und Darko Marinov (2002), "Evaluating the small scope hypothesis"
  4. ↑ University of Washington PLSE Neutrons, UW PLSE Neutrons
  5. ↑ Pamela Zave: Reasoning about identifier spaces: How to make Chord correct, in: IEEE Trans. Software Engineering 43, 12 (Dec. 2017), 1144–1156.
  6. ↑ Akhawe, D., Barth, A., Lam, P.E., Mitchell, J. and Song, D.: Towards a formal foundation of Web security, in: Proceedings of the 23rd IEEE Computer Security Foundations Symp. Edinburgh, 2010, 290–304.
  7. ↑ Dennis, G., Chang, F. and Jackson, D.: Modular verification of code with SAT, in: Proceedings of the Intern. Symp. Software Testing and Analysis, Portland, ME, Juli 2006.
  8. ↑ Dennis, G., Yessenov, K. and Jackson, D.: Bounded verification of voting software, in: Proceedings of the 2nd IFIP Working Conf. Verified Software: Theories, Tools, and Experiments. Toronto, Okt. 2008.
  9. ↑ Protocol Design with Alloy, auf haslab.github.io
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.