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. Mehr zur Spezifikation von Dynamik in Alloy
        Quellen zum Beispiel einer anderen Spezifikation der Filesharing-App ⇗
   3. Temporale Logik
        Die Semantik temporaler Operatoren ⇗
   4. Beispiel eines verteilten Algorithmus
        Quellen zur Spezifikation des Ring-Algorithmus ⇗
        Quellen zur Verifikation des Ring-Algorithmus ⇗
   5. Temporale Logik
        Die Semantik temporaler Operatoren ⇗
        Quellen zu den temporalen Operatoren ⇗
       
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: 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