Unterschiede

Hier werden die Unterschiede zwischen zwei Versionen angezeigt.


—lehre:abschlussarbeiten:untersuchungen_zum_anwendungspotential_der_formalen_verifikation [2024/10/30 03:13] (aktuell) – angelegt - Externe Bearbeitung 127.0.0.1
Zeile 1: Zeile 1:
 +====== Untersuchungen zum Anwendungspotenzial der formalen Verifikation im Bereich Motorsteuerungssoftware ======
 +~~NOTOC~~
 +===== Aufgabenstellung =====
  
 +Automotive Software unterliegt hohen Qualitätsanforderungen und wird mit entsprechendem Aufwand entwickelt. Trotzdem treten in Einzelfällen Fehler erst spät im Entwicklungsprozess oder sogar im Feld zu Tage, die bei den zahlreichen Qualitätssicherungsmaßnahmen nicht erkannt wurden. Die mit der Entwicklung befassten Unternehmen sind daher an Methoden interessiert, die diese Situation verbessern können.\\
 +\\
 +<style center>{{:lehre:abschlussarbeiten:siemens_vdo.gif|}}</style>
 +\\
 +\\
 +Ein möglicher Ansatz zur frühzeitigen Fehlererkennung ist die Methode der formalen Verifikation. Sie ist seit mehreren Jahrzehnten Forschungsthema und es stehen mittlerweile Erfolg versprechende Werkzeuge zur Verfügung, ihre Etablierung im Bereich Automotive Software steht aber noch aus.\\
 +\\
 +Das Thema der Diplomarbeit ist daher die Untersuchung, welche Möglichkeiten die formale Verifikation zur Fehlervermeidung in der Entwicklung von Automotive Software bietet. Den Ausgangspunkt werden reale Fehlerdaten für hardwarenahe Software in Motorsteuergeräten bilden, die vom Industriepartner Siemens-VDO zur Verfügung gestellt werden. Auf dieser Basis und mit der Möglichkeit, weitere Informationen von Entwicklern zu erfragen, soll die Frage beantwortet werden, ob die betreffenden Fehler bei systematischem Einsatz formaler Verifikationsmethoden (vor allem Modelchecking) gefunden worden wären. Zusammen mit einer Aufwandsbetrachtung und Analyse von Alternativen ist dann zu bewerten, welche methodischen Verbesserungen durch fomale Verifikation zu erzielen sind.\\
 +\\
 +Die Diplomarbeit wird gemeinsam mit Siemens-VDO in Regensburg durchgeführt. Sie erfordert sowohl Aufenthalte in Regensburg als auch in Aachen.
 +
 +===== Student =====
 +
 +  * [[:lehrstuhl:mitarbeiter:polzer]]
 +
 +===== Betreuer =====
 +
 +  * [[:lehrstuhl:mitarbeiter:schlich]]