ASCET-VERIFY Formale Verifikation von ASCET-SD-Modellen (Sorry - this page is only available in German.)

Goal

ASCET-SD ist ein von der Firma ETAS vertriebenes CASE-Tool zur Entwicklung eingebetteter Software-Systeme. Dieses Werkzeug wird von BMW in der Entwicklung unterschiedlicher Steuergeräte eingesetzt. Auf der anderen Seite ist BMW seit Jahren am Einsatz formaler Verifikationstechniken interessiert und ist von den in OFFIS entwickelten Verifikationstechniken überzeugt. Hieraus ergab sich der Wunsch die OFFIS-Verifikationsumgebung für ASCET-SD einsetzen zu wollen. Dies führte zu einer Kooperation zur Entwicklung einer prototypischen Anbindung von ASCET-SD an die Verifikationstechnik. Unter Einbeziehung von ETAS wurde in diesem Projekt die Anbindung realisiert. In einer Bestandsaufnahme wurden ASCET-SD-Modelle analysiert und eine geeignete Teilklasse für die Anbindung identifiziert.

Darüber hinaus wurde der Einsatz dieses Werkzeuges an einem Fallbeispiel erprobt. Hierzu wurde ein Teilmodul der aktuellen Entwicklung der AFS-Software ausgewählt. Mit der für den neuen 5er BMW entwickelten Aktivlenkung AFS (Active Front Steering) erfolgt der Einstieg in die „Steer-by-Wire“-Technik. Innerhalb des Projektes wurden ausgewählte Eigenschaften der sogenannten Failsafe-Komponente überprüft, d.h. ob z.B. bei einer Störung des Systems die Aktivlenkung sicher abgeschaltet wird.

In der laufenden Weiterentwicklung geht es darum einerseits noch fehlende Elemente zu integrieren, ein benutzerfreundliches Interface zu schaffen, ein Management der Beweisaufgaben zu realisieren und die Performance des Werkzeuges zu erhöhen.

Persons

Duration

Start: 31.12.2001
End: 30.12.2005