Die Informatik des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Verwaltung des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Informatik des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Mathematik des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Universität Bremen


INHALT & PFAD:
Startseite Detail

Bild: Zum Thema ''

Model Checking von Speicher-bezogenen Eigenschaften für Hardware/Software Codesigns



Datum: 29.07.2014
Uhrzeit: +++ ACHTUNG NEUE ZEIT +++ 13.00 Uhr c.t.

Ort: Cartesium Rotunde


Vortragende(r): Marcel Pockrandt Homepage - Vortragende(r) (Fachgebiet Programmierung Eingebetteter Systeme, Technische Universität Berlin)

Hardware/Software Codesign hat in den vergangen Jahren stark an Einfluss gewonnen und wird inzwischen auch häufig im industriellen Systementwurf eingesetzt. Insbesondere findet es dort ebenfalls im sicherheitskritischen Bereich Anwendung. Für solche Systeme ist Testen allein nicht ausreichend. Obwohl bereits Ansätze zur formalen Verifikation von HW/SW Codesigns bestehen, werden wichtige Teilaspekte wie Speicher dort zumeist nur teilweise unterstützt. Im Rahmen dieses Vortrages wird ein Ansatz zur vollautomatischen Transformation von SystemC/TLM Modellen in äquivalente UPPAAL Timed Automata Modelle vorgestellt. Dabei verwenden wir ein formales Speichermodell, welches die formale Darstellung einer großen Anzahl an Speicher-bezogenen Operationen und Konstrukten ermöglicht. Zusätzlich generieren wir vollautomatisch Eigenschaften für die formale Verifikation mit dem UPPAAL Model Checker, mit denen die Abwesenheit einer großen Zahl von typischen Speicherzugriffsfehlern wie beispielsweise Nullpointer Zugriffe oder Double Frees verifizieren können.

Biografie

Marcel Pockrandt studierte bis 2009 Informatik an der Technischen Universität. Für seine Diplomarbeit erhielt er 2010 den Preis der GI Fachgruppe Test, Analyse und Verifikation von Software(TAV). Seit Dezember 2009 ist er als wissenschaftlicher Mitarbeiter im Fachgebiet Programmierung eingebetteter Systeme unter der Leitung von Prof. Sabine Glesner an der TU Berlin angestellt. Seine Forschungsinteressen liegen in der Modellierung und vollautomatischen Verifikation von SystemC/TLM Modellen sowie der Analyse des Speicherverhaltens.



Ansprechpartner(in) / Einladende(r):
Prof. Dr. Rolf Drechsler


Download:




zurück  

Seitenanfang  -  Impressum Zuletzt geändert durch: jungmann [b]   28.07.2014 Admin-Login