“Correctness by Construction” für die Konsolidierung auf Multicore Prozessoren

In meiner Promotion entwickele ich einen methodischen Ansatz weiter, der sich bereits mehrfach in der Entwicklung sicherheitskritischer Systeme bewährt hat. Er verbirgt sich hinter dem Motto “Correctness by Construction” und versucht eine schrittweise Formalisierung des Entwicklungsprozesse zu erreichen, um damit automatisierte Verifikationen zu ermöglichen, so dass die Fehlerraten um Größenordnungen gesenkt werden.

Währten dieser Ansatz bisher im Bereich der Software-Entwicklung eingesetzt wurde, arbeite ich an einer Erweiterung auf die Integration von sicherheitskritischen Anwendungen auf einem Multicore oder Manycore Prozessor. Die Grundidee bleibt dabei natürlich erhalten: das korrekte Verhalten kann anhand der Entwicklungsschritte nachgewiesen werden und muss nicht umständlich die Analysen des Verhalten gezeigt werden.

Ich glaube nicht, dass man mit vollständiger Formalisierung des Entwicklungsprozesses die Anforderungen heutiger Systeme bändigen kann. Dafür sind die Entwicklungszyklen zu kurz und die Anforderungskataloge zu kurz. Dennoch bin ich davon überzeugt, dass gerade die Komplexität von Mehrkernprozessoren zu einer verstärkten Akzeptanz von punktuell eingesetzten, formalen Methoden führen wird. Diese müssen dann natürlich auch durch den Fachexperten nutzbar gestaltet sein. Kann man denn eine formale Spezifikation in Z für eine kritische ECU von einem Automotive-Entwickler erwarten? Ich denke nicht.

Tags »

Autor:
Datum: Mittwoch, 5. Oktober 2011 14:28
Trackback: Trackback-URL Themengebiet: Forschung & Promotion, Modellierung, Multicore

Feed zum Beitrag: RSS 2.0 Kommentare sind geschlossen,
aber Du kannst einen trackback auf Deiner Seite setzen.

Keine weiteren Kommentare möglich.