Formale Verifikation eines komplexen seriellen Kommunikationsprotokolls – „Lessons Learned“ am Beispiel einer FlexRay-IPVerifikation

Konferenz: Zuverlässigkeit und Entwurf - 2. GMM/GI/ITG-Fachtagung
29.09.2008 - 01.10.2008 in Ingolstadt, Germany

Tagungsband: Zuverlässigkeit und Entwurf

Seiten: 2Sprache: DeutschTyp: PDF

Persönliche VDE-Mitglieder erhalten auf diesen Artikel 10% Rabatt

Autoren:
Kimmeskamp, Thorsten; Jochim, Markus; Formann, Johannes; Echtle, Klaus (Universität Duisburg-Essen, Arbeitsgruppe Verlässlichkeit von Rechensystemen, 45141 Essen)
Bulach, Slava; Weinberger, Katharina (Robert Bosch GmbH, GB Automotive Electronics, 72703 Reutlingen)

Inhalt:
Da sicherheitskritische Systeme im Fehlerfall eine Gefahr für Leib und Leben darstellen können, ist oftmals ein exakter Nachweis der geforderten Zuverlässigkeit angezeigt. Eine der dabei nutzbaren Methoden ist das Bounded Model Checking, welches bereits erfolgreich bei der Verifikation von Prozessoren eingesetzt wurde. Um nun am Beispiel von E-Ray, einer von Bosch entwickelten IP des Kommunikationsprotokolls FlexRay, auch auf neuen Gebieten Praxiserfahrungen zu sammeln, haben sich Bosch und die Universität Duisburg-Essen im Rahmen des BMBF-Projektes „HERKULES“ zusammengetan.