Logik und formale Methoden TI5002
»Spezifizieren, Modellieren und Überprüfen von Systemen
mittels angewandter Logik«
Übersicht
Materialien
Portable Document Format, 296 KB, Stand 22.03.2011
Portable Document Format, 457 KB, Stand 15.12.2010
Portable Document Format, 287 KB, Stand 10.12.2010
Portable Document Format, 511 KB, Stand 28.01.2011
7-Zip Archivdatei, 30098 KB, Stand 1.04.2011
Übungen/Praktikum
Werkzeuge
MPA
Der MPA (MNI Proposition Analyzer) ist ein Werkzeug zur Analyse von Formeln der Aussagenlogik. Es kann zur Überprüfung eines Teils der Übungsaufgaben eingesetzt werden, sowie zu den Anwendungen im Teil der Vorlesung über die Aussagenlogik, insbesondere das Variabilitätsmodell für Softwareproduktlinien.
Jape
Jape ist ein Werkzeug, mit dem man interaktiv Herleitungen des natürlichen Schließens entwickeln kann.
Ich habe spezielle Anpassungen von Jape gemacht und auch die Aufgaben aus den Übungsblättern eingebaut:
Alloy
Alloy ist ein Model Finder, mit dem man Modelle von Software analysieren kann. Wir setzen Alloy im Teil der Vorlesung über die Prädikatenlogik ein.
Der Ansatz von Alloy wird in folgendem Buch beschrieben: Daniel Jackson Software Abstractions: Logic, Language, and Analysis MIT Press, 2012.
Spin
Spin ist ein Model Checker, jSpin eine Java-Oberfläche für Spin. Wir setzen Spin im Teil der Vorlesung über temporale Logik ein.
Am einfachsten installiert man Spin auf Basis der Distribution von jSpin von Moti Ben-Ari auf der
Der Ansatz von Spin und die Verwendung von jSpin wird in folgendem Buch beschrieben: Mordechai Ben-Ari Principles of the Spin Model Checker Springer, 2008.