Ergänzende Informationen zum Buch
Formale Modelle der Softwareentwicklung
Model-Checking, Verifikation, Analyse und Simulation
erschienen im Vieweg+Teubner Verlag
Buchbeschreibung (mit Genehmigung des Verlages)
Software muss funktionieren, um von Kunden akzeptiert zu werden. Doch wie stellt man sicher, dass die Steuerung
eines Raumschiffs, eines Herzschrittmachers oder einer Aktienverwaltung korrekt funktioniert? Neben den
klassischen Testansätzen spielen für den Korrektheitsnachweis zunehmend formale Modelle eine zentrale Rolle.
Ein Modell erlaubt es, ein beliebiges sequenzielles oder verteiltes System zu analysieren und zu simulieren.
Dadurch, dass Korrektheitsanforderungen präzise definiert werden, kann man sogar verifizieren, dass die
Anforderungen erfüllt sind. Dieses Buch stellt unterschiedliche formale Modelle mit ihren Einsatzmöglichkeiten
und Werkzeugen vor. Dabei steht bewusst die Anwendung der Modelle und nicht die Theorie dahinter im Vordergrund.
Alle Kapitel schließen mit Wiederholungsfragen und Übungsaufgaben.
Der Inhalt
Motivation von Formalen Modellen - Modelchecking mit PROMELA und SPIN - Modelchecking mit Timed Automata und Uppaal
- Petrinetze - Programmverifikation
Vorwort, Inhaltsverzeichnis, Ausschnitte aus Beispielkapiteln und Stichwortverzeichnis als PDF
Ergänzende Bemerkungen
Formale Modelle sind ein sehr guter Ansatz, die Qualität von Systemen zu erhöhen. Dieses Buch gibt eine Einführung in
verschiedene Ansätze, wobei das praktische Exeperimentieren im Vordergrund steht. Anders als andere Bücher zu diesem
Themengebiet werden nur grundlegende Erfahrungen in der Programmierung und etwas Logik-Kenntnisse vorausgesetzt;
auf eine intensive Beschäftigung mit den theoretischen Grundlagen wird verzichtet. Der Grad der Formalität nimmt
im Buch zu. Für praktische Übungen stehen Werkzeuge zur Verfügung, die zumindest für das Selbststudium frei erhältlich sind.
Das Buch entstand als Ergebnis mehrerer Vorlesungen für Studierende höheren Semesters.
Das Buch wurde insbesondere geschrieben für:
- Informatik-Studierende ab 4. Semester
- Studierende in Informatik-orientierten Masterstudiengängen
- Entwickler kritischer Systeme
- QS-erfahrene Praktiker, die sich kompakt über den aktuellen Stand der Technologie informieren wollen
Das Buch ist so konzipiert, dass es sich auch für das Selbststudium eignet.
Der genaue Einsatz des Buches hängt vom Studiengang und Veranstaltungsumfang ab. In Studiengängen mit
Informatikschwerpunkt sollte es möglich sein, zumindest den Stoff des ersten und drei der folgenden vier Kapitel
mit kleinen Abstrichen
in einer zweistündigen Lehrveranstaltung unterzubringen. Weitere Kürzungen sind möglich.Generell ist es sinnvoll, weitere
Beispiele oder Beispiele des Buches schrittweise an der Tafel zu entwickeln.
Material zum Buch
Die Abbildungen des Buches liegen im Powerpoint-, emf- oder eps-Format vor.
Weiterhin gibt es einen vollständigen Foliensatz, der eng angelehnt am Buch entwickelt wurde.
Die Lösungen zu den Aufgaben des Buches liegen im PDF-Format vor.
Alle Informationen können unter Beachtung des Copyrights des Verlages und des Autoren
für Lehrveranstaltungen genutzt werden.
Errata
Korrekturen und Klarstellungen von Lesern werden gerne angenommen und an dieser Stelle veröffentlicht.
Die aktuelle Errata-Version ist 1.1.
Werkzeuge
- Generell kann hier eine detaillierte Anleitung
herunter geladen werden.
- Zur Spezifikation, Simulation und Verifikation verteilter Systeme wird
SPIN genutzt. Um SPIN unter
Windows laufen zulassen, wird ein C-Compiler und eine TCL-Installation benötigt.
TCL kann als
ActiveTCL konstenfrei zum Lernen bezogen werden.
Zur Installation eines C-Compilers wird MinGW
unter dieser Adresse geladen.
Nach der Installationmuss der Pfad zum C-Compiler in die
Pfad-Variable aufgenommen werden, meist C:\MinGW\bin.
SPIN kann hier herunter geladen werden,
evtl. funktioniert dieser Link.
Das Zip-File kann irgendwo ausgepackt werden. Die Datei spin.exe muss in ein Verzeichnis kopiert
werden, das in der Pfadvariablen eingetragen ist, z.B. C:\MinGW\bin (oder Pfad zum
SPIN-Verzeichnis in den PFAD eintragen). Danach kann ispin oder xspin im Auspackverzeichnis
gestartet werden.
- Zur Spezifikation, Simulation und Verifikation verteilter Systeme mit Zeit wird
Uppaal und damit Timed Automata (Realzeitautomaten) eingesetzt.
Das Werkzeug kann von der Uppaal-Seite kostenfrei bezogen werden. Es setzt eine lauffähige Java 6-Version (oder neuer) voraus.
Nach dem Entpacken kann Uppaal durch einen Doppelklick auf uppaal.jar gestartet werden. Solle dies nicht möglich sein
und ein Pack-Programm das jar-File öffnen, müssen Sie entweder dem Pack-Programm mitteilen, dass es keine jar-Dateien
öffnen soll oder in das Uppaal-Verzeichnis wechseln, um das Programm mit
java -jar uppaal.jar zu starten.
- Zur Spezifikation und Simulation von Petri-Netzen wird das Werkzeug
NetLab genutzt,
das leider nur für Windows erhältlich ist. Der Werkzeug wird von der RWTH Aachen im
Institut für Regelungstechnik
entwickelt. Eventuell funktioniert folgender
Direkt-Link zum Herunterladen.
Zurück zur Kleuker-Hauptseite