Automotive Formale Beschreibung und Modelltransformation von Taskkonfigurationen einer Motorsteuerung

Die formale Verifikation der Integrität dynamischer Eigenschaften von Echtzeitsystemen gewinnt immer mehr an Bedeutung. Dieser Artikel beschreibt eine Modelltransformation zur Generierung von Petri-Netzen aus der Taskkonfiguration von Motorsteuerungen.

Anbieter zum Thema

MES Electronic Connect GmbH & Co. KG

Cadlog Group

Eurocircuits GmbH

Bei der Entwicklung von Motorsteuerungssystemen im Automotive-Umfeld müssen statische sowie dynamische Aspekte des Systems in Betracht gezogen werden. Im Gegensatz zu der statischen Architektur eines Systems kann die dynamische Architektur in den etablierten Entwicklungsprozessen nur validiert werden, indem man vollständig implementierte Systeme intensiven Testprozeduren unterzieht, wie z.B. Hardware-in-the-Loop-Simulationen.

Um die Kosten, die durch eine Beseitigung von temporalen Fehlern in einem späten Entwicklungsstadium entstehen, so gering wie möglich zu halten, ist es notwendig eine Aussage bezüglich der Integrität des dynamischen Verhaltens einer Motorsteuerung zu einem möglichst frühen Zeitpunkt zu treffen. Mögliche Zeitpunkte sind z.B. sobald die Tasks definiert sind und Funktionalitäten den einzelnen Tasks zugeordnet werden und die Planungsphase des Tasksystems und die Zuordnung von Funktionalitäten.

Der in diesem Artikel am Beispiel einer Verbrennungsmotorsteuerung beschriebene Ansatz beinhaltet das Verwenden von Modelltransformationen um die Lücke zwischen einer semi-formalen Beschreibung (Task-Modell) und einer formal verifizierbaren Repräsentation einer Task-Konfiguration eines Systems zu überbrücken. Diese formale Repräsentation, hier Petri Netze, dient als Zielmodell der Transformation und kann später zur Verifizierung der Integrität der dynamischen Aspekte des Systems verwendet werden.

Um das Verhalten des Systems so genau wie möglich modellieren zu können, wurde ein OSEK-konformes Betriebssystem eingehend analysiert und darauf folgend ein Meta-Modell zur Darstellung aller wichtigen Aspekte als Petri Netz spezifiziert. Das Petri Netz seinerseits wurde mit Hilfe der Petri Net Markup Language (PNML) Syntax (Billington, 2003) beschrieben.

Das Quellmodell der Transformation, die semi-formale Beschreibung der Task-Konfiguration des Systems, wird mit Hilfe eines Editors erstellt. Es beinhaltet Informationen die aus dem Quellcode des Systems, aus den Projektdefinitionen des Systems und aus Messungen der Ausführungszeiten von einzelnen Softwarefunktionen gewonnen werden können.

Die komplette Modelltransformation ist in ein Plug-In für die Eclipse IDE integriert. Das Ziel- und Quellmodell für die Modelltransformation wurden mit Hilfe des Eclipse Modeling Frameworks (EMF) und mit dem ihm zugrunde liegenden Meta-Modells ECore definiert. Die Transformation wurde mit der QVT Operational Modelltransformationssprache implementiert und durchgeführt, welche, wie das EMF, als Open Source Software in Form eines Eclipse Plug-Ins vorliegt.

Beschreibung der Methodik

Nachfolgend sind die Prozessschritte der vorgeschlagenen Verifikationsprozedur beschrieben. Abbildung 1 zeigt diesen Ablauf graphisch. Ein Task-Modell des Motorsteuerungssystems wird in einem dafür bereitgestellten Editor erstellt. Dieses Modell wird mit allen, für die Verifikation benötigten Daten angereichert, wie z.B. den Ausführungszeiten der Softwarefunktionen.

Nach der Fertigstellung eines solchen Modells wird dieses nun in ein korrespondierendes Petri Netz transformiert. Es handelt sich hierbei um ein priorisiertes, zeitbehaftetes Petri Netz, das mit Hilfe der PNML Syntax beschrieben wird. Auf einer abstrakteren Ebene wurde zuvor ein Meta-Modell definiert indem alle für die Verifikation benötigten Strukturen durch Petri Netz Elemente beschrieben sind.

(ID:25368550)