Es ist schon beeindruckend, wie sicher Autos, Flugzeuge und Züge heutzutage sind. Betrachtet man dies, so scheint es, als würden wir sehr gut verstehen, wie man zuverlässige Systeme baut. Das liegt unter anderem an Sicherheitsstandards. Wenn diese nicht eingehalten werden, wie es bei Toyota der Fall gewesen zu sein scheint, kann es schiefgehen. Sicherheitsstandards entwickeln sich aus zwei Gründen weiter: Sie entwickeln sich weiter, da wir mehr über Sicherheit lernen, und sie entwickeln sich weiter, da sie sich an die Komplexität heutiger Systeme anpassen müssen. Deshalb empfahl man, formale Methoden einzusetzen.
Bevor wir uns mit formalen Methoden und deren Bezug zu Anforderungen befassen, geben wir einen Überblick über Sicherheitsstandards. Die folgende Abbildung wurde aus dem Deploy Wiki übernommen, was eine ganze Menge Analyse liefert.
Von besonderem Interesse ist die IEC 61508, da sie als Grundlage für domänenspezifische Standards wie die ISO 26262 dient. Sie führt beispielsweise das Konzept der Safety Integrity Levels (SIL) ein, ein relatives Maß für die Risikominderung, die eine Sicherheitsfunktion bietet. Mit anderen Worten, die SIL-Stufe schreibt vor, wie zuverlässig eine Funktion sein muss, von SIL 1 (niedrig) bis SIL 4 (hoch).
Die Normen erkennen an, dass die Verwendung formaler Methoden kostspielig ist, aber sie erkennen auch das Potenzial von formalen Methoden an. Es ist kein Wunder, dass sich die Normen daher auf SIL 4 in Bezug auf formale Methoden konzentrieren. Infolgedessen werden in der IEC 61508 formale Methoden für SIL 4-Funktionen “dringend empfohlen”. Die EN 50128 (Schiene) empfiehlt sie sogar für SIL 1 und 2 und spricht für SIL 3 und 4 eine “dringende Empfehlung” aus. Tatsächlich ist die Bahnindustrie führend bei der Einführung formaler Methoden.
Eine interessante Ausnahme ist die ISO 26262, die formale Methoden “empfiehlt”, aber semi-formale Methoden “dringend empfiehlt”. Laut der obigen Quelle lag dies an Lobbyarbeit der Automobilindustrie, die sich um die Kostenüberschreitung sorgte.
Was ist mit den formellen Anforderungen?
Wenn wir über formale Methoden sprechen, meinen wir typischerweise, dass die Systembeschreibung – die Spezifikation – formalisiert wurde. Anforderungen bilden einen erheblichen Teil der Systembeschreibung. In der Praxis gibt es zwei Ansätze: Entweder werden die Anforderungen ebenfalls formalisiert, oder es besteht eine Rückverfolgbarkeit zwischen nicht-formalen Anforderungen und der formalen Spezifikation.
Während die Formalisierung von Anforderungen möglich ist, ist die Akzeptanz gering. Selten sind Stakeholder bereit, die Formalismen zu lernen, um die Anforderungen zu verstehen. Nichtsdestotrotz ist es wichtig zu erkennen, dass das Lesen formaler Modelle viel einfacher ist als das Erstellen. In sicherheitskritischen Bereichen ist es möglicherweise möglich, den Kunden davon zu überzeugen, in die Schulung der Stakeholder zum Lesen der formalen Spezifikationen zu investieren. Das Schreiben kann auf einen kleinen Kreis von Experten beschränkt werden.
Der entgegengesetzte Ansatz ist, die Anforderungen informell zu halten, aber eine Rückverfolgbarkeit zum formalen Modell herzustellen. Dies wird oft von den Stakeholdern bevorzugt, erfordert aber Disziplin bei der Aktualisierung der Rückverfolgbarkeit, insbesondere im Hinblick auf das Änderungsmanagement. Der Wunsch, dies zu tun, spiegelt sich im Erfolg von wider SysML, ein Dialekt von UML, der die Konzepte von Anforderungen und Anforderungstransparenz umfasst.
Nahtlose Nachverfolgbarkeit
Anstatt sich dem statischen Rückverfolgbarkeitsmodell von SysML zu ergeben, lohnt es sich, alternative Rückverfolgbarkeitsmodelle zu erkunden. Wir bei Formal Mind haben einen Ansatz entwickelt, der den Stakeholdern ausreichend Raum lässt, ihre Anforderungen in natürlicher Sprache auszudrücken, während Bereitstellung einer Struktur, die die Rückverfolgbarkeit in einem formalen Modell (in diesem Fall Event-B) systematisch und skalierbar macht. Es gibt natürlich unzählige weitere Ansätze, und die Herausforderung besteht darin, den richtigen Ansatz für das jeweilige Projekt zu finden (und dabei die bestehenden Prozesse zu berücksichtigen).
Eine wichtige Voraussetzung für Skalierbarkeit ist die Tool-Unterstützung, und Eclipse bietet eine leistungsstarke Plattform für die Integration verschiedener Werkzeuge zur nahtlosen Rückverfolgbarkeit, wie wir zuvor gezeigt haben. Diese Lösungen wurden mithilfe von Open-Source-Tools realisiert, und natürlich gibt es auch viele kommerzielle Lösungen für die Rückverfolgbarkeit (wie reqtify oder agosense, um nur zwei zu nennen). Nichtsdestotrotz enthält Eclipse einige branchenübliche Komponenten, wie RMF/ProR, die in Produktionsumgebungen eingesetzt werden. Alternativ ermöglicht Eclipse, kostengünstig schnell Prototypen zu erstellen, um verschiedene Ansätze zu erkunden.
Mehr Informationen
Wir regelmäßig unser Wissen veröffentlichen und bei öffentlichen Veranstaltungen präsentieren, wie kürzlich bei TdSE (organisiert von der deutschen Sektion von INCOSE), und hoffentlich nächstes Jahr auf der ReConf 2014.Wir bieten auch interne Schulungen und Workshops an, die Themen wie funktionale Sicherheit, Sicherheitsstandards, Anforderungsrückverfolgbarkeit oder formale Modellierung abdecken. Bitte Kontaktieren Sie uns um herauszufinden, wie wir Sie produktiver machen können.
Bild mit freundlicher Genehmigung von tungphoto / FreeDigitalPhotos.net
