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.
![]() |
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 |