Interaktives Spezifizieren und Verifizieren von Softwareartefakten SE5021

Model Finding und Model Checking mit Alloy

Mit der Prädikatenlogik kann man Strukturen präzise spezifizieren, auch die Dynamik, d.h. die Transitionen in Softwaresystemen kann man logisch beschreiben durch die Spezifikation der Struktur von Zustand und Folgezustand. Model Finding bedeutet das Generieren von Modellen für die Spezifikationen. Mit temporaler Logik werden erwünschte oder unerwünschte Eigenschaften dynamischer Systeme formuliert. Model Checking besteht darin, zu überprüfen ob solche Eigenschaften in gegebenen Modellen erfüllt sind oder nicht.

Alloy ist eine Sprache mit der man Strukturen und ihre Transitionen sowie temporale Eigenschaften spezifizieren kann. Der Alloy Analyzer visualisiert die spezifizierten Modelle und erlaubt so interaktives Spezifizieren und Verifizieren.

Inhalt

1. Erste Begegnung mit Alloy 6
   1. Zum Anfang ein (leichtes) Rätsel
   2. Ein Beispiel: Serialisierbarkeit von Transaktionen in Datenbanken
   3. Prinzipien des formalen Designs mit Alloy
   4. Wie arbeitet Alloy?
   5. Anwendungen von Alloy
2. Design der Struktur eines Systems in Alloy
   1. Konzepte am Beispiel der Spezifikation eines Dateisystems
   2. Relationale Logik
3. Design der Dynamik eines Systems in Alloy
   1. Konzepte am Beispiel der Spezifikation eines verteilten Algorithmus
   2. Temporale Logik
4. Aufbau von Alloy-Spezifikationen
   1. Die Sprache von Alloy - Referenz
   2. Vordefinierte Module
   3. Miscellanea
5. Interessante Beispiele von Spezifikationen mit Alloy
   1. Euklidischer Algorithmus
   2. Zwei-Phasen-Commit-Protokoll
   3. Needham-Schroeder Authentifizierungsprotokoll
   4. Echo-Algorithmus zum Erstellen eines Spannbaums eines Graphen

Moodle-Kurs zur Veranstaltung ⇗

Materialien

Burkhardt Renz: Die Hard in Electrum. THM, Juni 2021 Portable Document Format, 728 KB, Stand 17.10.2023

Burkhardt Renz: Quelle zu Die Hard in Electrum. Juni 2021 Alloy Source, 1 KB, Stand 18.03.2024

Burkhardt Renz und Nils Asmussen: Kurze Einführung in Alloy. 2010 - 2019, Technische Hochschule Mittelhessen Portable Document Format, 416 KB, Stand 17.10.2023

Burkhardt Renz: Spezifikation von Strukturen in Alloy am Beispiel Dateisystem. März 2023 Zip Archivdatei, 10 KB, Stand 17.10.2023

Burkhardt Renz: Spezifikation von Strukturen: Ausdrücke und Operatoren der relationalen Logik. März 2023 Zip Archivdatei, 7 KB, Stand 17.10.2023

Burkhardt Renz: Spezifikation von Dynamik in Alloy am Beispiel Ring-Algorithmus. März 2023 Zip Archivdatei, 9 KB, Stand 17.10.2023

Burkhardt Renz: Verifikation von Spezifikationen in Alloy am Beispiel Ring-Algorithmus. Mai 2023 Zip Archivdatei, 3 KB, Stand 17.10.2023

Burkhardt Renz: Temporale Operatoren in Alloy. THM, Mai 2023 Portable Document Format, 230 KB, Stand 17.10.2023

Burkhardt Renz: Lineare temporale Logik in Alloy. Mai 2023 Zip Archivdatei, 4 KB, Stand 17.10.2023

Burkhardt Renz: Erste Begegnung mit Alloy 6. THM, Juni 2023 Portable Document Format, 5579 KB, Stand 17.10.2023

Burkhardt Renz: Quellen zum Echo-Algorithmus. April 2022 Zip Archivdatei, 5 KB, Stand 17.10.2023

Burkhardt Renz: Übungen. April 2023 Portable Document Format, 489 KB, Stand 10.03.2024