Formale Spezifikation für sicherheitskritische Anforderungen

Was wäre, wenn Ihr Computer Ihre Anforderungen versteht?

BTC EmbeddedSpecifier

Formale Spezifikation für sicherheitskritische Anforderungen

BTC EmbeddedSpecifier ist ein Werkzeug für die Erstellung und Verwaltung von semi-formalen und formalen Anforderungen in sicherheitskritischen Projekten. Während die semi-formale und formale Beschreibung von Anforderungen im ISO 26262 und IEC 61508 Standard empfohlen wird, ist für das Lesen und Schreiben der Anforderungen, in den meisten formalen Beschreibungssprachen ein umfangreiches Expertenwissen notwendig. Dies ändert sich nun dank BTC EmbeddedSpecifier. Den Ausgangspunkt des Formalisierungsprozesses bildet die informale textuelle Anforderung, welche sich tool-gestützt Schritt für Schritt und intuitiv in eine formale Anforderung ableiten lässt.

Formalisierte Anforderungen = Bessere Anforderungen

In heutigen Entwicklungsprojekten werden Anforderungen in der Regel in einer informellen, natürlichen Sprache beschrieben und in Tools wie IBM DOORS oder PTC Integrity verwaltet. Da die natürliche Sprache grundsätzlich einen gewissen Interpretationsspielraum mit sich bringt, kann es vorkommen, dass Funktionsentwickler oder Testingenieure ein anderes Verhalten implementieren, als ursprünglich geplant war. Mit Hilfe einer semi-formalen oder formalen Beschreibung im BTC EmbeddedSpecifier werden Anforderungen in eine klare, eindeutige und maschinenlesbare Darstellung überführt. Dies erhöht zum Einen die Qualität der Anforderungen und steigert zusätzlich ihren Wert für die weitere Verwendung im Entwicklungsprozess.

Universal Pattern - Willkommen in der formalen Welt

Unserer Erfahrung nach gibt es in erster Linie zwei Gründe, weshalb die formale Beschreibung von Anforderungen bislang noch keine besonders große Akzeptanz in Softwareentwicklungsprojekten für eingebettete Systeme gefunden hat. Zum einen wird der Umgang mit formalen Sprachen wie LTL als zu schwierig wahrgenommen und zum anderen bieten diese Sprachen selbst keine ausreichenden Möglichkeiten, die Nachverfolgbarkeit zu den bestehenden informellen Anforderungen im Projekt sicherzustellen. Mit Universal Pattern werden diese beiden Aspekte effizient adressiert. Ein typischer Workflow beginnt mit dem Import von natürlich-sprachlichen Anforderungen. Im ersten Schritt werden individuelle Ausdrücke oder Ereignisse als sog. Makros im Text identifiziert. Im zweiten Schritt werden diese Makros strukturiert, um deren Beziehung und zeitliches Verhalten abzubilden. Daraus resultiert - als Zwischenergebnis - eine semi-formale Beschreibung. Sie beginnen grundsätzlich mit einer einfachen Struktur, welche Sie dann falls notwendig verfeinern, um die formale Anforderung so einfach wie möglich aber so komplex wie nötig zu beschreiben. Eine grafische Darstellung dient als Editor und zugleich als Dokumentation, so dass die Anforderungen immer überprüfbar und nachvollziehbar sind. Im letzten Schritt werden die Makros mit echten Interfaceobjekten des zu testenden Systems verknüpft und sind damit maschinenlesbar.

Eine aussagekräftige Definition der Requirement Coverage

Bei natürlich-sprachlichen Anforderungen ist die Definition der Requirements Coverage immer eine schwierige Frage. Da die Anforderungen nicht maschinenlesbar sind, beruht die Entscheidung ob eine Anforderung abgedeckt ist und ob diese Abdeckung vollständig ist in der Regel auf einem manuellen Review der zugehörigen Testfälle.

Auf Basis der Spezifikationsmethode Universal Pattern haben wir nun eine neue mathematische Definition der Requirement Coverage entwickelt, welche eine vollständig automatische Berechnung der Requirement Coverage ermöglicht.

Formalisierte Anforderungen = Bessere Verifikation

Aufgrund der Maschinenlesbarkeit von formalisierten Anforderungen können diese in verschiedenen Verifikationsmethoden eingesetzt und damit die Qualität und die Vollständigkeit des Verifikationsprozesses dramatisch erhöht werden. Beispiele dafür sind:

BTC EmbeddedSpecifier bietet weiterhin zwei Add-Ons, um die formalisierten Anforderungen als sog. „Requirement Observers“ zu exportieren. Diese können wiederum in andere Testumgebungen importiert werden, um dort die Einhaltung der Anforderungen automatisiert sicher zu stellen. Die Observer können entweder als C-Code exportiert werden oder in das dSPACE RTT Format, um in Echtzeit auf einer dSPACE Plattform ausgeführt zu werden.