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. Die Sprache von Alloy - Referenz
   2. Vordefinierte Module
   3. Miscellanea
5. Interessante Beispiele von Spezifikationen mit Alloy
   1. Euklidischer Algorithmus
   2. Needham-Schroeder Authentifizierungsprotokoll
   3. Zwei-Phasen-Commit-Protokoll

Materialien

Burkhardt Renz: Temporale Operatoren in Alloy. THM, Februar 2022 Portable Document Format, 230 KB, Stand 9.02.2022

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, Mai 2022 Portable Document Format, 5575 KB, Stand 17.05.2022

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

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

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

Burkhardt Renz: Spezifikation von Dynamik in Alloy am Beispiel Ring-Algorithmus. Januar 2022 Zip Archivdatei, 9 KB, Stand 21.01.2022

Burkhardt Renz: Verifikation von Spezifikationen in Alloy am Beispiel Ring-Algorithmus. Januar 2022 Zip Archivdatei, 3 KB, Stand 21.01.2022

Burkhardt Renz: Lineare temporale Logik in Alloy. Januar 2022 Zip Archivdatei, 4 KB, Stand 27.01.2022

Burkhardt Renz: Übungen. Juni 2022 Portable Document Format, 388 KB, Stand 20.06.2022