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
   1. Zum Anfang ein (leichtes) Rätsel
        Das Rätsel ⇗
        Die Lösung in Alloy ⇗
        Mehr zu »Die Hard in Alloy« ⇗
   2. Prinzipien des formalen Designs mit Alloy
   3. Ein weiteres Beispiel: Serialisierbarkeit von Transaktionen in Datenbanken
        Alloy Diskussionsseite ⇗
        Serialisierbarkeit in Datenbanken ⇗
        Serialisierbarkeit in Alloy ⇗
   4. Wie arbeitet Alloy?
        Konzept Alloy ⇗
        Architektur von Alloy ⇗
   5. Anwendungen von Alloy
        Daniel Jackson Alloy: a language and tool for exploring software designs ⇗
2. Design der Struktur eines Systems in Alloy
   1. Konzepte am Beispiel der Spezifikation eines Dateisystems
        Quellen zum Beispiel des Dateisystems ⇗
   2. Relationale Logik
        Quellen zu Ausdrücken und Operatoren der relationalen Logik ⇗
3. Design der Dynamik eines Systems in Alloy
   1. Konzepte am Beispiel der Spezifikation einer Filesharing-App
        Quellen zum Beispiel der Filesharing-App ⇗
   2. Temporale Logik
   3. Beispiel eines verteilten Algorithmus
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 und Nils Asmussen: Kurze Einführung in Alloy. 2010 - 2019, Technische Hochschule Mittelhessen Portable Document Format, 432 KB, Stand 18.04.2024

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

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

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

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

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