Forschungsbericht 2014 - Max-Planck-Institut für Softwaresysteme, Standort Kaiserslautern

Auf der Suche nach einer „Statik” für das Computerzeitalter

Autoren
Brandenburg, Björn B.
Abteilungen
Real-Time Systems Group
Zusammenfassung
Computer stecken heutzutage in allen modernen Technologien: Sie beobachten, sie steuern, sie entscheiden. Wenn alles gut geht, halten sie Autos in der Spur und unbemannte Luftfahrzeuge in der Luft. Doch was passiert, wenn etwas schief geht? Wenn die allgegenwärtigen Rechner, sogenannte cyber-physische Systeme, fehlerhaft sind? Um sicherzustellen, dass zukünftige Technologien auch im Computerzeitalter beherrschbar bleiben, entwickeln Forscher am Max-Planck-Institut für Softwaresysteme Grundlagen für nachweisbar fehlerfreie cyber-physische Systeme.

Ob man es nun ubiquitous computing, pervasive computing oder neuerdings Internet of Things nennt, es ist offensichtlich, dass der Einsatz von eingebetteten (also auf den ersten Blick unsichtbaren) und vernetzten Computersystemen in allen Bereichen des modernen Lebens unaufhörlich voranschreitet. Das birgt neben vielen Chancen auch einige Risiken.

Denn Rechner tun nicht immer das, was sie sollen. Zwar mag man bei ärgerlichen Missgeschicken, wie zum Beispiel einem „intelligenten” Thermostat, das versehentlich zu viel oder zu wenig heizt, oder einem „intelligenten” Kühlschrank, der unentwegt Milch nachbestellt, vielleicht einfach nur lachen, den Kopf schütteln und sich fragen, ob man denn solche Spielereien wirklich braucht. Doch der Spaß hört spätestens dann auf, wenn die Sicherheit von Menschen oder die Verfügbarkeit grundlegender Infrastruktur auf dem Spiel stehen.

Man denke zum Beispiel an die kommende Generation von drive-by-wire Technologien, bei denen die klassische mechanische Steuerung von Kraftfahrzeugen immer weiter durch leichtere, flexiblere, digital vernetzte Steuersysteme ersetzt wird: Offensichtlich ist die allzeit korrekte und sichere Funktion solcher Steuersysteme essentiell. Ebenso muss die Bordelektronik von Fluggeräten einwandfrei funktionieren und allzeit stabiles und kollisionsfreies Fliegen garantieren. Ähnlich kritische Computersysteme finden sich bei der Kontrolle und Überwachung von Industrieanlagen, Energienetzen und im Bahn- und Schiffsverkehr, um nur ein paar Bereiche des täglichen Lebens zu nennen.

Cyber-physische Systeme — Schlüsseltechnologie des 21. Jahrhunderts

Als übergeordneter Begriff für derartige Systeme hat sich in den letzten Jahren das Schlagwort cyber-physische Systeme (engl. cyber-physical systems) eingebürgert. Darunter versteht man komplexe, meist vernetzte, computerbasierte Systeme, die ihre physische Umgebung wahrnehmen bzw. messen und auf sie reagieren, um sie aktiv zu beeinflussen. Die schon genannten Steuergeräte in Fahrzeugen sind typische Beispiele solcher Systeme, wie auch die Steuerung und Kontrolle von Energienetzen und Industrieanlagen.

Bei genauerer Betrachtung stellt man fest, dass nahezu alle modernen Schlüsseltechnologien cyber-physische Komponenten verwenden und somit ihren Sinn und Zweck ohne Einsatz von Computern nicht mehr erfüllen können. Kurz: Schon heute vertrauen wir täglich unser Wohlergehen computergesteuerten Systemen an, und es ist zu erwarten, dass unsere Abhängigkeit von cyber-physischen Systemen in Zukunft weiterhin rasant zunehmen wird (wenn z. B. selbstfahrende PKWs Serienreife erlangen).

Die gesamtgesellschaftliche Relevanz von cyber-physischen Systemen ist demnach nicht zu unterschätzen, und so ist es auch nur konsequent, dass sie einer der Forschungsschwerpunkte am Max-Planck-Institut für Softwaresysteme (MPI-SWS) in Kaiserslautern und Saarbrücken sind.

Grundlegende Fragen der Sicherheit

Aus Sicht der Grundlagenforschung steht dabei die Frage der funktionalen Sicherheit (engl. functional safety) im Vordergrund: Wie kann man sicherstellen, dass ein solches System in der Praxis tatsächlich „immer das Richtige” macht, also nicht „versehentlich” durch Fehler im System die Benutzer oder die Umgebung in Gefahr bringt?

Diese Frage stellt sich gleich zweimal: einerseits für die Ingenieure/-innen, die das System entwickeln — wie entwirft und konstruiert man cyber-physische Systeme, die effizient und sicher funktionieren? Und andererseits im Rahmen von Prüf- und Genehmigungsverfahren (z. B. einer Zertifizierung durch den TÜV) — wie kann man Dritten gegenüber nachweisen, dass die Realisierung eines cyber-physischen Systems auch tatsächlich die gewünschten Eigenschaften gewährleistet und die vorgeschriebenen Sicherheitsstandards einhält?

Insbesondere der zweite Aspekt — das Problem der Nachweisbarkeit — gewinnt zunehmend an Bedeutung. Denn um sicherzustellen, dass auch komplexe, computerbasierte Technologien beherrschbar bleiben, braucht es fundierte Prinzipien, Methoden und Berechnungsverfahren, aufgrund derer man Fehlverhalten in allen erdenklichen Situationen a priori ausschließen kann.

Dabei muss man zwischen zwei grundsätzlichen Anforderungen unterscheiden. Zunächst müssen cyber-physische Systeme richtig funktionieren, und zwar in dem Sinne, dass sie die spezifizierten Reaktionen auf externe Stimuli und sich ändernde Umgebungsbedingungen zeigen. Darüber hinaus müssen sie aufgrund ihrer oftmals engen Kopplung mit physikalischen Prozessen in der realen Welt auch rechtzeitig reagieren. Um einen sicheren Betrieb zu gewährleisten, müssen cyber-physische Systeme beide Kriterien erfüllen, denn eine prinzipiell richtige, also logisch korrekte Reaktion kann nutzlos oder sogar schädlich sein, wenn sie verspätet eintritt.

Die Relevanz beider Anforderungen kann man leicht anhand eines Airbags verdeutlichen: Er muss im Falle eines Unfalls zuverlässig auslösen (und auch nur dann), und er muss es zum exakt richtigen Zeitpunkt tun, denn Sekundenbruchteile können den Unterschied zwischen der korrekten Positionierung des Luftkissens und einem Systemversagen ausmachen. Auch wenn ein Airbag ein ungewöhnlich dramatisches Beispiel sein mag, kann man allgemein festhalten, dass eine zuverlässige und sichere Steuerung von physikalischen Prozessen ein korrektes Zeitverhalten des cyber-physischen Systems voraussetzt — die Realität wartet nicht auf den Computer.

Nachweisbar sichere cyber-physische Systeme

Das Kriterium, richtig zu reagieren, bezeichnet man als logische Korrektheit (engl. logical correctness) eines Systems, das Kriterium, rechtzeitig zu reagieren, als temporale Korrektheit (engl. temporal correctness). Fokus der Grundlagenforschung zu cyber-physischen Systemen am MPI-SWS ist die Entwicklung von praxistauglichen Algorithmen und Methoden, die es erlauben, formal analysierbare (engl. analytically sound) cyber-physische Systeme zu konstruieren, deren logische und temporale Korrektheit mittels mathematischer Beweise nachgewiesen werden kann.

Entscheidend ist dabei die mathematische Beweisbarkeit: Analog zur mechanischen Statik, mit der man unter gewissen Annahmen die Stabilität eines Gebäudes nachweisen kann, sind Systeme, die unter gewissen Annahmen beweisbar logisch und temporal korrekt sind, inhärent fehlerfrei. In der Praxis ist ein solch hoher Sicherheitsstandard zwar größtenteils noch Zukunftsmusik, doch umso wichtiger ist es, jetzt die nötigen Grundlagen für die angestrebte „cyber-physische Statik” zu entwickeln, also die Basis für ein zukünftiges umfassendes Kalkül für nachweislich korrekte cyber-physische Systeme zu schaffen.

Im Jahrbuch der MPG 2013 wurden bereits einige relevante Resultate mit Bezug auf die logische Korrektheit beschrieben, daher steht im Folgenden das Zeitverhalten im Mittelpunkt, das durch ein aktuelles Projekt illustriert wird.

Wie lang ist die Warteschlange?

Beim Nachweis der temporalen Korrektheit eines Systems entstehen besondere Komplikationen durch Prozesse, die Betriebsmittelkonflikte (engl. resource conflicts oder mutual exclusion requirements) haben, also durch Prozesse, die exklusiven Zugriff auf Ressourcen benötigen, die auch von anderen Prozessen von Zeit zu Zeit (exklusiv) genutzt werden. In einem solchem Fall spricht man von einem geteilten Betriebsmittel (engl. shared resource), das sich zwei oder mehrere Prozesse teilen, indem sie abwechselnd Zugriff erlangen. Dabei kann es sich um Datenstrukturen (z. B. einen Nachrichtenpuffer oder eine Datenbank, in der aktuelle Sensorwerte hinterlegt werden) handeln, um Teile des Betriebssystems (z. B. einen Netzwerktreiber) oder um spezielle Eingabe-/Ausgabegeräte (z. B. Datenleitungen, an die Sensoren angeschlossen sind).

Wenn nun zwei oder mehrere Prozesse zeitgleich versuchen, auf ein geteiltes Betriebsmittel zuzugreifen, muss das Betriebssystem die Zugriffe serialisieren — es bildet sich eine Schlange, in der die Prozesse warten müssen, bis sie mit ihrem Zugriff an der Reihe sind. Offensichtlich ist das Warten in der Schlange ein potentielles Risiko, da es zu inakzeptablen Verzögerungen führen kann. Um nachzuweisen, dass ein cyber-physisches System temporal korrekt ist, ist es deshalb notwendig, eine obere Schranke für die maximale Wartezeit jedes Prozesses zu ermitteln.

Die tatsächliche maximale Wartezeit hängt von einer Vielzahl von Faktoren ab und kann a priori nicht exakt bestimmt werden, da einige der relevanten Faktoren erst zur Laufzeit in Erfahrung zu bringen sind (z. B. die genauen Zeitpunkte, zu denen die Prozesse aktiviert werden). Das Ziel der Wartezeitanalyse ist es stattdessen, eine sichere Schätzung der längsten Wartezeit (engl. worst-case blocking time) so vorzunehmen, dass die ermittelte Schranke größer ist als alle zur Laufzeit tatsächlich auftretenden Wartezeiten. Dabei soll die Schranke aus Gründen der Effizienz natürlich möglichst wenig vom realen Maximum abweichen.

Um eine hinreichend genaue Schätzung zu erlangen, muss einerseits zur Laufzeit ein berechenbares Protokoll zur Betriebsmittelallokation eingesetzt werden (z. B. first-in first-out, „wer zuerst kommt, mahlt zuerst”), und andererseits a priori eine möglichst exakte Analyse aller statisch bekannten Parameter durchgeführt werden. Am MPI-SWS wird dieser Themenkomplex unter mehreren Gesichtspunkten erforscht. So wurden zum Beispiel neue Protokolle zum Verwalten geteilter Betriebsmittel entwickelt, die besonders gute Eigenschaften bezüglich der maximalen Wartezeit aufweisen [1-3]. Weiterhin wurden neue Analysemethoden zur Begrenzung der maximalen Wartezeit entwickelt, die mithilfe linearer Optimierung wesentlich genauere Schranken liefern [4, 5]. Darüber hinaus konnten Schranken für einige in der Praxis weit verbreitete Protokolle ermittelt werden, die vormals als „unberechenbar” galten [5]. Außerdem wurden Fragen der Effizienz sowohl in theoretischer [6] als auch in praktischer Hinsicht untersucht [7].

Eine allumfassende „Statik” für sichere cyber-physische Systeme ist damit zwar noch nicht gefunden — doch als Wegbereiter für eine Zukunft, in der sicherheitskritische Computersysteme nachweislich fehlerfrei sind, ist Grundlagenforschung zu logischer und temporaler Korrektheit, wie sie am MPI-SWS durchgeführt wird, unabdingbar.

Literaturhinweise

Brandenburg, B. B.
A fully preemptive multiprocessor semaphore protocol for latency-sensitive real-time applications
Proceedings of the 25th Euromicro Conference on Real-Time Systems (ECRTS 2013), 292–302 (2013)
DOI: 10.1109/ECRTS.2013.38
Brandenburg, B. B.
The FMLP+: An asymptotically optimal real-time locking protocol for suspension-aware analysis
Proceedings of the 26th Euromicro Conference on Real-Time Systems (ECRTS 2014), 61–71 (2014)
DOI: 10.1109/ECRTS.2014.26
Brandenburg, B. B.
A synchronous IPC protocol for predictable access to shared resources in mixed-criticality systems
Proceedings of the 35th IEEE Real-Time Systems Symposium (RTSS 2014) 196–206 (2014)
DOI: 10.1109/RTSS.2014.37

Brandenburg, B. B.
 

Improved analysis and evaluation of real-time semaphore protocols for P-FP scheduling
 

Proceedings of the 19th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2013), 141–152 (2014)
DOI: 10.1109/RTAS.2013.6531087

Wieder, A.; Brandenburg, B. B.
On spin locks in AUTOSAR: blocking analysis of FIFO, unordered, and priority-ordered spin locks
Proceedings of the 34th IEEE Real-Time Systems Symposium (RTSS 2013), 45–56 (2013)
DOI: 10.1109/RTSS.2013.13
Wieder, A.; Brandenburg, B. B.

On the complexity of worst-case blocking analysis of nested critical sections
Proceedings of the 35th IEEE Real-Time Systems Symposium (RTSS 2014), 106–117 (2014)
DOI: 10.1109/RTSS.2014.34
Spliet, R.; Vanga, M.; Brandenburg, B. B. ; Dziadek, S.
Fast on Average, Predictable in the Worst Case: Exploring Real-Time Futexes in LITMUSRT
Proceedings of the 35th IEEE Real-Time Systems Symposium (RTSS 2014), 96–105 (2014)
DOI: 10.1109/RTSS.2014.33
Zur Redakteursansicht