Formale Verifikation eines komplexen seriellen Kommunikationsprotokolls – „Lessons Learned“ am Beispiel einer FlexRay-IPVerifikation
Conference: Zuverlässigkeit und Entwurf - 2. GMM/GI/ITG-Fachtagung
09/29/2008 - 10/01/2008 at Ingolstadt, Germany
Proceedings: Zuverlässigkeit und Entwurf
Pages: 2Language: germanTyp: PDF
Personal VDE Members are entitled to a 10% discount on this title
Authors:
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)
Abstract:
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.