Zum Inhalt springenZur Suche springen

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

Rodin

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.

ProB

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/

EvalB

Dies ist eine Art einfache Online-Version von ProB, um prädikatenlogische Formeln ausprobieren zu können.

Literatur

Rodin Handbuch

Das Handbuch handelt sowohl über die Software Rodin als auch über Event-B. Es beinhaltet ein Tutorial sowie Referenzkapitel.

The B Method von Steve Schneider

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.

EventB Summary

Überblick auf vier Seiten über die Event-B Syntax.

Rodin Modelle

Modelle für Abrials Event-B Buch.

Verantwortlichkeit: