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 Textformat


Für den Fall, dass Ihr Computer das entsprechende Format nicht angezeigen kann, können Sie sich hier das Dokument als unformatierte Textausgabe ansehen.

(Bitte haben Sie dafür Verständnis, dass gewisse Dokumente nicht als Textalternative zur Verfügung stehen.)


Download:
Download Model Checking von Speicher-bezogenen Eigenschaften für Hardware/Software Codesigns (application/pdf 214.9 KB)


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




Einladung zum Vortrag


29. Juli 2014, 13.00 Uhr c.t.
Universität Bremen | Cartesium Rotunde



Marcel Pockrandt
Fachgebiet Programmierung Eingebetteter Systeme, Technische Universität Berlin


Model Checking von Speicherbezogenen Eigenschaften für
Hardware/Software Codesigns
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 Speicherbezogenen 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.

Dieser Gast wurde von Rolf Drechsler eingeladen.
Telefon: 21863932


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


 



zurück  




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