imported>Gak69: Weblink aus Fließtext entfernt

2022-05-15T22:56:21Z

Weblink aus Fließtext entfernt

Neue Seite

{{Infobox Software
| Name = Alloy Analyser
| Logo =
| Screenshot = [[Datei:Screenshot of Alloy Analyzer.png|240px]]
| Beschreibung = Screenshots mit Beispiel
| Maintainer = [[Daniel Jackson (Informatiker)|Daniel Jackson]]
| Hersteller =
| Management =
| AktuelleVersion = 6.0.0
| AktuelleVersionFreigabeDatum = 4. November 2021
| AktuelleVorabVersion =
| AktuelleVorabVersionFreigabeDatum =
| Betriebssystem = [[plattformunabhängig]]
| Programmiersprache = [[Java (Programmiersprache)|Java]]
| Kategorie =
| Lizenz = [[MIT-Lizenz]]
| Deutsch = nein
| Website = [http://alloytools.org AlloyTools]
}}

Der '''Alloy Analyzer''' ist ein in der [[Informatik]] und [[Softwaretechnik]] eingesetztes Programm, das dazu genutzt werden kann, um [[Spezifikation]]en, die in der Sprache ''Alloy'' geschrieben sind, zu analysieren und zu simulieren.<ref name="jackson2012">{{Literatur | Autor=Daniel Jackson | Titel=Software Abstrations: Logic, Language, and Analysis | Verlag=[[MIT Press]] | Ort= | Jahr=2012 | ISBN=978-0262017152 }}</ref> Das Programm kann Modelle der Spezifikation (Modelle im Sinne der [[Modell (Logik)|formalen Logik]]) erzeugen, also Instanzen aller [[Invariante (Informatik)|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 [[Lineare temporale Logik|linearen temporalen Logik]] zur Verfügung<ref>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. </ref>.

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 [[Agile Softwareentwicklung|agilen]] Modellierung.

Die Sprache ''Alloy'' und der Alloy Analyzer werden seit 1997 unter der Leitung von [[Daniel Jackson (Informatiker)|Daniel Jackson]] am [[Massachusetts Institute of Technology]] in den USA entwickelt. Die Bezeichnung „Alloy“ (Deutsch: Legierung) rührt daher, dass ''Alloy'' von Konzepten der [[Z-Notation|Spezifikationssprache Z]] und des [[Model Checking]]s beeinflusst wurde.

== Analyseansatz ==

Die Sprache ''Alloy'' hat die Ausdrucksmächtigkeit der [[Prädikatenlogik erster Stufe]] erweitert um den [[Transitiver Abschluss|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''<ref name="jackson2012"/>, die besagt, dass ein hoher Anteil an [[Programmfehler]]n bereits gefunden werden kann, wenn man das Programm für alle Eingabewerte eines kleinen Gültigkeitsbereichs prüft.<ref>Alexandr Andoni, Dumitru Daniliuc, Sarfraz Khurshid und Darko Marinov (2002), "[http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.8.7702 Evaluating the small scope hypothesis]"</ref>

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.<ref name="jackson2012"/> 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 [[Symbolic Model Verifier|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.<ref>University of Washington ''PLSE Neutrons'', [http://neutrons.uwplse.org/ UW PLSE Neutrons]</ref>
* ''Netzwerk-Protokolle'': [[Pamela Zave]] konnte mit Hilfe des Alloy Analyzers Fehler in [[Chord]] finden und Korrekturen vorschlagen.<ref>Pamela Zave: Reasoning about identifier spaces: How to make Chord correct, in: ''IEEE Trans. Software Engineering 43'', 12 (Dec. 2017), 1144–1156.</ref>
* ''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.<ref>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.</ref>
* ''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<ref>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.</ref> sowie von Code eines elektronischen Wahlsystems<ref>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.</ref> eingesetzt.

== Beispiele ==

Eine Uhr (nur mit Stundenanzeige) in Alloy 6

<syntaxhighlight lang="text">
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
</syntaxhighlight>

Auswahl eines ausgezeichneten Knotens in einem Ring von Prozessen, siehe Julien Brunel, David Chemouil, Alcino Cunha, Nuno Macedo: Formal Software Design with Alloy 6.<ref>[https://haslab.github.io/formal-software-design/protocol-design/index.html#making-the-specification-more-abstract Protocol Design with Alloy], auf haslab.github.io</ref>

<syntaxhighlight lang="text">
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
</syntaxhighlight>

== Einzelnachweise ==
<references />

== Weblinks ==
* [http://alloytools.org Homepage von Alloy und Alloy Analyzer] am [[Massachusetts Institute of Technology|MIT]]
* [https://alloytools.discourse.group Alloy Diskussionsforum]
* [https://groups.csail.mit.edu/sdg/pubs/2019/alloy-cacm-18-feb-22-2019.pdf Daniel Jackson: ''Alloy: A Language and Tool for Exploring Software Designs''] in: ''Communications of the ACM'', September 2019
* [http://www.doc.ic.ac.uk/project/examples/2007/271j/suprema_on_alloy/Web/ Eine Anleitung für Alloy]
* [http://emina.github.io/kodkod/ Homepage des Kodkod Constraint Solver]
* [https://esb-dev.github.io/mat/alloy-intro.pdf Kurze Einführung in Alloy]
* [https://esb-dev.github.io/mat/echo.pdf Erste Begegnung mit Alloy 6]

[[Kategorie:Theoretische Informatik]]
[[Kategorie:Freies Programmierwerkzeug]]
[[Kategorie:Java-Programm]]

Alloy Analyzer - Versionsgeschichte

imported>Gak69: Weblink aus Fließtext entfernt