Dienstag, 23. April 2024

Archiv


Sicherheit für Winzlinge

So genannte Embedded Controller sind moderne, unsichtbare Heinzelmännchen, die den Alltag vereinfachen - vom Staubsauger bis zum Flugzeug. Das allerdings macht sie besonders empfindlich für Softwarefehler. Das Projekt Gesy in Bremen will hier zu mehr Qualität beitragen.

Von Holger Bruns | 13.01.2007
    GESy ist ein Doktorandenkolleg an der Universität Bremen, das sich die eingebetteten Systeme als Ziel gesetzt hat.

    Professor Rolf Drechsler von der Universität Bremen. Er kümmert sich um den sicheren Entwurf elektronischer Systeme, die zum Beispiel in Weichen und Stellwerken, Flugzeugen und Automobilen, aber auch in Haushaltsgeräten wie Herden und Waschmaschinen die Funktionen steuern. Das wird heute von Mikrocontrollern erledigt, die aus einem Prozessor, etwas Speicher und Anschlüssen für Leitungen bestehen. Diese Systeme werden aufgabenbezogen programmiert und sollten idealerweise fehlerfrei arbeiten, obwohl sie aus vielen Bauteilen bestehen, von denen jedes einzelne eine Fehlerquelle sein kann. Heutige Chips integrieren immerhin Hunderte von Millionen einzelner Transistoren, Tendenz steigend.

    Wie kann man trotz dieser zunehmenden Komplexität immer noch die ganze Software so gestalten, dass sie korrekt ist? Und aus Spezifikationen heraus gehen wir jetzt also her und übersetzen diese stückweise in ausführbare Programme. Und diese Übersetzung wird maschinell überwacht und überprüft. Dass wir also hier sicher sein können, dass nicht neue Fehler eingebaut werden.

    Diese Bearbeitungen werden mit speziellen Programmierwerkzeugen vorgenommen, die an der Universität Bremen zum Teil selbst entwickelt wurden. Die auf diese Weise entstehende Software wird jedoch nicht für sich alleine auf ihre Korrektheit hin überprüft, sie wird vielmehr zusammen mit den Systemen getestet, auf denen sie später zum Einsatz kommt, sagt Professor Jan Peleska.

    Für diese so genannten Hardware-Software-Integrationstests haben wir automatisierte Prüfverfahren entwickelt, die man "modellbasiertes Testen", eben analog zum modellbasierten Entwickeln nennt. Unsere Testsoftware interpretiert automatisch die Soll-Spezifikation des Systems, inklusive Bedingungen für Reihenfolgen, Zeitbedingungen und Bedingungen über kontinuierliche Abläufe, entwickelt daraus automatisch Sequenzen von Eingabedaten, mit denen der Testling, also Hardware plus Software zusammen zu Reaktionen provoziert wird, und prüfen automatisch, ob diese Reaktionen in Bezug auf Werte, Reihenfolgen und Zeitbedingungen spezifikationskonform sind.

    Allerdings hat das bloße Testen eines Systems einige Nachteile. Es ist nicht daran zu denken, dass man alle eventuellen Fehler nur durch Probieren findet. Wegen dieser Unsicherheit entspricht der Testaufwand also ungefähr dem Entwicklungsaufwand, was Geld kostet, sagt Jan Peleska, und denkt auch an einen anderen Weg.

    Wir haben, ausgehend von Standardformalismen, wie zum Beispiel UML, Erweiterungen entwickelt, die einmal ermöglichen, besonders präzise und auf einfachere Art Sicherheitsbedingungen und Echtzeitbedingungen für solche Steuerungssysteme zu spezifizieren, und zweitens auf der Ebene dieser Spezifikation bereits den grundsätzlichen Sicherheitsnachweis zu führen. Das heißt, die Frage, ob in einem Stellwerksbereich zwei Signale fehlerhaft auf "freie Fahrt" gestellt werden können, so dass es potentiell zu einer Zugkollision kommen kann, diese Frage kann bereits auf der logischen Ebene der Spezifikation geklärt werden.

    Die modellgetriebene Softwareentwicklung verringert den Zeitaufwand für die Programmierung dramatisch und verbessert gleichzeitig die Qualität des Zielcodes, der automatisch aus den Modellierungen heraus erzeugt wird. Einige Fragen bleiben allerdings weiterhin offen und sind heuer Gegenstand der aktuellen Forschung. Professor Rolf Drechsler:

    Man muss leider heute sagen, wir können für sehr komplexe Systeme die Korrektheit nicht garantieren. Aber das ist das Ziel. Darauf arbeiten wir hin, dass so etwas gelingen kann.

    Die so sehr gefürchteten Fehler in der Software vor allem sicherheitsrelevanter Systeme werden also gezielt handzahm gemacht und verlieren so ihre Bedrohlichkeit. Das Graduiertenkolleg "eingebettete Systeme" ist in erster Linie ein universitäres Projekt, das den Teilnehmern die Promotion in zwei bis drei Jahren ermöglichen soll. Doch es gibt weitere Pläne.

    Andererseits haben wir natürlich das Ziel, hier attraktiv auch gerade für Unternehmen auch hier aus der Region zu sein, um eben diese Technologie in die entsprechenden Firmen zu bekommen und auch eine Perspektive zu geben, auch in Form von Weiterbildung.