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. Ausgehend von einer informalen textuellen Anforderung wird die formale Spezifikation Schritt für Schritt und intuitiv abgeleitet. Wie im ISO 26262 Standard empfohlen, kann die somit maschinenlesbare Spezifikation anschließend zur formalen Verifikation verwendet werden.

Features:

  • Intuitive semi-formale und formale Anforderungsspezifikation
  • Direkte Anbindung an Requirements-Management Tools wie DOORS oder PTC Integrity zur Verknüpfung von informalen und formalen Anforderungen
  • Durchgängige Traceability durch konsequentes Verlinken der Artefakte
  • Export von Requirement Observern zur Einbindung in beliebige Test Umgebungen (z.b. dSPACE VEOS oder dSPACE HIL Systeme)
  • Automatische Generierung von Testfällen zur Abdeckung der Requirements
        
        
        

Beispiel für die Spezifikation mit Simplified Universal Pattern

        

Die Grafik links bezieht sich auf die folgende informale Anforderung eines Fensterhebers im Auto:

Wenn, für mindestens 50ms, ein Hindernis erkannt wurde (obstacle is detected), muss das Signal zum Absenken des Fensters (window down signal) für mindestens 1 Sekunde aktiviert werden. “.

Nachdem die richtige Interpretation (Progress, Ordering oder Invariant; in diesem Fall Progress) des "Unviersal Pattern" ausgewählt wurde, müssen vom Anwender der “Trigger” und die “Action” parametrisiert werden. Dabei müssen der zeitliche Verlauf und die feststehende Bedingung berücksichtigt werden.

Für eine “Semi-formale Sepzifikation” werden direkt im Text der Anforderung - durch eine einfach zu bedienende Interaktion - die beiden folgenden Makros definiert:

  1. “[…] obstacle is detected […]”-> ObstacleDetected
  2. “[…] window down signal […]” -> WindowDown

Das Makro “ObstacleDetected” wird zur “Trigger Condition” und das Makro “WindowDown” wird verwendet um die “Action Condition” zu definieren.

Die zeitlichen Definitionen werden direkt wie im Text angegeben festgelegt: 50ms (Trigger Duration), 10ms (Scope Duration) und 1000ms (Action Duration) als Echtzeitbeschreibung.

Um nun den Level einer “Formalen Spezifikation” zu erreichen, müssen die beiden Makros mit einer echte “Interface Beschreibung” verknüpft werden. Das sind Signale wie “Input”, “Output”, “Local” und “Calibration” Variablen des zu verifizierenden Systems (System Under Verification).

Wenn dieser Level erreicht wurde, sind sowohl die Syntax als auch die Semantik der Anforderungsbeschreibung eindeutig definiert.



Kontakt

Vereinbaren Sie einen Termin mit uns.

Tel: +49 441 96 97 38-0

E-Mail: info@btc-es.de