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. Spezifikation und Verifikation des Echo-Algorithmus
   3. Prinzipien des formalen Designs mit Alloy 6
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. Ausdrücke
   2. Prädikate und Funktionen
   3. Module
   4. Kommandos
5. Interessante Beispiele von Spezifikationen mit Alloy
   1. ??? -- noch auszuwählen

Materialien

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

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

Burkhardt Renz: Erste Begegnung mit Alloy 6. THM, Dezember 2021 Portable Document Format, 5568 KB, Stand 3.12.2021

Burkhardt Renz: Quellen zum Echo-Algorithmus. November 2021 Zip Archivdatei, 5 KB, Stand 8.12.2021

Burkhardt Renz: Spezifikation von Strukturen in Alloy am Beispiel Dateisystem. Januar 2022 Zip Archivdatei, 10 KB, Stand 11.01.2022

Burkhardt Renz: Spezifikation von Strukturen: Ausdrücke und Operatoren der relationalen Logik. Januar 2022 Zip Archivdatei, 7 KB, Stand 13.01.2022