Formale Beschreibung und Modelltransformation von Taskkonfigurationen einer Motorsteuerung

Anbieter zum Thema

MES Electronic Connect GmbH & Co. KG

Cadlog Group

Eurocircuits GmbH

Die Erkenntnisse, die aus dem Model Checking gewonnen werden dienen dem Software-Entwickler als Maß für die dynamische Integrität seines Modells. Die dynamische Integrität wird in verschiedenen Stufen bezüglich des geschätzten Verhaltens des Systems unter realen Bedingungen kategorisiert und im Editor angezeigt. Diese Bewertung dient den Entwicklern zur Unterstützung bei der Behebung von dynamischen Problemen.

Petri Netze

Petri Netze sind eine formale Methode um dynamische Systeme mit nebenläufigen und nichtdeterministischen Prozessen zu modellieren, zu analysieren und zu simulieren. Petri Netze werden als gerichtete, bipartite Graphen mit den Knotentypen Stelle und Transition dargestellt (Petri, 1962). Stellen können Marken aufnehmen und Transitionen konsumieren Marken von Stellen (Eingabestellen) bzw. produzieren Marken auf Stellen (Ausgabestellen). Eine Transition feuert (d.h. sie konsumiert und produziert Marken) wenn alle Eingabestellen mit der ausreichenden Anzahl an Marken ausgestattet sind.

Zusätzlich zu normalen Kanten an denen Marken konsumiert bzw. produziert werden existieren noch zwei andere Kantentypen: Inhibitor- und Testkanten. Inhibitorkanten bewirken, dass eine Transition nur feuern kann wenn die Stelle, auf die die Inhibitorkante zeigt keine Marke hat. Eine Testkante bewirkt, dass die Transition nur feuern kann wenn die Stelle, auf die die Testkante zeigt eine Marke hat. Im Gegensatz zu einer normalen Kante wird die Marke aber nicht beim Feuern der Transition konsumiert.

Petri Netze können mit zusätzlichen Elementen erweitert werden, um komplexere Szenarien zu modellieren. Zwei Erweiterungen, die in unserem Ansatz Verwendung finden, sind nachfolgend beschrieben:

• Das Hinzufügen von Prioritäten zu Petri Netzen wird durch eine zusätzliche Kantenart realisiert. Jeweils zwei Transitionen werden mit diesen Prioritätskanten verbunden um eine Prioritätsrelation herzustellen. Die Transition von der die Kante entspringt ist von höherer Priorität als die Transition, in die die Kante mündet. Daraus folgt dass die Transition niedriger Priorität nur dann feuerbar ist wenn die höher priorisierte Transition nicht feuern kann.

• Um dynamische Systeme korrekt zu modellieren, werden bei zeitbehafteten Petri Netzen (Berthomieu, 1991) Transitionen mit Verzögerungen ausgestattet. Diese Verzögerungen sind Intervalle mit den Grenzen ( entspricht der unteren bzw. oberen Grenze des Intervalls). Die Verzögerungsintervalle führen zu einem veränderten Verhalten der Transitionen: Sobald eine Transition nach den Regeln eines Standard Petri Netzes feuerbar wäre, wird das Feuern um den im Verzögerungsintervall definierten Wert verzögert.

Modellierung und Modelltransformation

Im oben beschriebenen Verifikationsprozess wird eine Transformation von einem semi-formalen Modell zu einem formalen, verifizierbaren Modell vollzogen. Dafür müssen diese Modelle durch ein Meta-Modell definiert werden.

Quellmodell: In diesem Modell ist das System ausschließlich aus Tasks und deren Bestandteilen aufgebaut. Es enthält folgende Elemente:

• OsTask: Ein OsTask repräsentiert einen Betriebsystemtask. Er beinhaltet alle Attribute, die im OSEK Standard definiert sind (OSEK/VDX, 2005).

• Runnable: Ein Runnable ist eine elementare Softwarefunktion, normalerweise eine C-Funktion. Die Ausführungszeit dieser Runnables muss vorher gemessen werden oder auf Basis von Schätzungen festgelegt werden.

• Software-Komponente: Runnables sind in Software Komponenten zusammengefasst, welche komplette Systemfunktionen, wie z.B. die Ermittlung der Kühlmitteltemperatur sprich Motortemperatur, repräsentieren.

• Task Sektion: In einem kooperativem Tasksystem, wie es in der vorliegenden Anwendung verwendet wird, sind die OsTasks in Sektionen mit einer vorher definierten maximalen Ausführungszeit unterteilt. Nach jeder Sektion wird der Scheduler explizit aufgerufen um einen Taskwechsel zu ermöglichen.

Das Modell enthält außerdem noch zahlreiche Elemente, die zur korrekten Darstellung im Editor, zur Festlegung von Versionen und zur Verwaltung von Software Komponents bzw. Runnables dienen.

Zielmodell

Das Zielmodell ist eine Repräsentation des Tasksystems und eines OSEK-konformen Schedulers. Dazu wurde das Scheduling-Verhalten von OSEK untersucht und mit Petri Netz Elementen beschrieben.

Ein solches System hat folgende Teilkomponenten:

• Task Activation: Hier werden die Instanzen der Taskaktivierungen durch eine Transition in vorher definierter Periodizität erzeugt. Es ist möglich die erste Taskaktivierung durch einen Offset zu verzögern um Häufungen von Taskaktivierungen zu vermeiden.

• Priority Queue: Sind multiple Taskaktivierungen für eine Task möglich, so müssen diese in einer Queue gespeichert werden. Tasks gleicher Priorität teilen sich eine Priority Queue.

• Task Start & Ausführung: Beim Start einer Task wird die Ressource (Prozessor) in Anspruch genommen. Während der Ausführung wird die Ressource nach jeder Task Section wieder freigegeben um einen Taskwechsel zu ermöglichen. Nach Beendigung der Task-Ausführung wird die Ressource endgültig freigegeben.

• Ressource: Die Ressource ist im Allgemeinen der Prozessor und wird während der Ausführung eines Tasks belegt.

(ID:25368550)