Sicherheitskritische Systeme
Inhalt
Soft- und Hardwaresysteme nehmen in der heutigen Gesellschaft einen wichtigen Platz ein. Diese Systeme werden immer häufiger für sicherheitskritische Anwendungen eingesetzt, bei welchen ein Fehlverhalten schwerwiegende Auswirkungen haben kann. Beispiele hierfür sind eingebettete Computer in modernen Autos, die zunehmend Einfluss auf das Fahrverhalten nehmen, sowie moderne Zugbeeinflussungssysteme oder Steuerungen für fahrerlose Zugsysteme.
Das Halbmodul "Sicherheitskritische Systeme" gibt eine Einführung in die Entwicklung von Softwaresystemen mit Hilfe von formalen Methoden am konkreten Beispiel der B-Methode.
Software
Wir werden diese Software zur formalen Modellierung verwenden. Sie ist für Linux/Windows und MacOS zu haben. Bitte installieren Sie die Version 3.3.
Wir setzen diese hier am Lehrstuhl entwickelte Software ein, um unsere Modelle zu analysieren. Über den Eclipse-Update-Mechanismus lässt sich innerhalb von Rodin ProB installieren. Die Update Seite für die neueste Version lautet wie folgt:
Für Rodin 3.x: ProB Nightly - http://nightly.cobra.cs.uni-duesseldorf.de/rodin3/updatesite/
Dies ist eine Art einfache Online-Version von ProB, um prädikatenlogische Formeln ausprobieren zu können.
Literatur
Das Handbuch handelt sowohl über die Software Rodin als auch über Event-B. Es beinhaltet ein Tutorial sowie Referenzkapitel.
Diese Buch behandelt die klassische B Methode. Wir werden uns in der Vorlesung voraussichtlich nicht mit klassischem B sondern mit Event-B beschäftigen, allerdings lassen sich die Kapitel über mathematische Grundlagen (z.B. Mengenlehre, Relationen, Funktionen) auf Event-B gut übertragen. Sie eignen sich mit vielen Beispielen und Übungen auch gut zum Selbststudium. In der Universitäsbibliothek liegen einige Exemplare.
Überblick auf vier Seiten über die Event-B Syntax.
- Rodin Modelle
Modelle für Abrials Event-B Buch.