SCODE-Methode

Mit der SCODE-Methode, die durch den SCODE-ANALYZER unterstützt und umgesetzt wird, werden Fehler beim Entwurf des Systems durch eine formale Verifikation im Werkzeug angezeigt und können sofort korrigiert werden. Somit können die Entwickler immer auf einem formal verifizierten System arbeiten. Experten können die Ergebnisse nutzen, um bereits bestehende Software zu optimieren oder neue Software zu entwerfen und die Testbarkeit zu verbessern.

Alle Ergebnisse können in unterschiedlicher Form durch weitere Werkzeuge weiterverarbeitet werden. Dies schließt die automatische Generierung von Programmcode ein.

Die SCODE-Methode

Beschreibung des Problemraums

Die SCODE-Methode ist ein dreistufiger, iterativer Prozess, mit dem ein System einfach dargestellt und analysiert werden kann. Ziel der Methode ist es, ein Problem in kleinere, voneinander unabhängig lösbare Probleme zu zerlegen, um über die Lösung der kleinen Probleme das große Problem zu lösen. SCODE-ANALYZER führt durch den Prozess und unterstützt aktiv.

Schritt 1 – Problemraum definieren

Im ersten Schritt wird der Problemraum definiert. Als Eingaben gelten dabei alle Aspekte des Systems oder der Systemumgebung, die eine Veränderung im System hervorrufen (z. B. Benutzereingaben, Messergebnisse von Sensoren). Ausgaben sind die hervorgerufenen Systemveränderungen (z. B. veränderte Variablen oder Signale)

Schritt 2 – Modi festlegen

Modi definieren

Im zweiten Schritt werden die gültigen und ungültigen Systemmodi beschrieben. Ein Modus wird durch die Kombination der ausgewählten Alternativen je Dimension definiert.

Dabei können unterschiedliche Kombinationen in den Eingangsdimensionen identische Kombinationen in den Ausgangsdimensionen ergeben; das bedeutet, dass unterschiedliche Eingaben gleiche Systemveränderungen hervorrufen.

SCODE-ANALYZER unterstützt und prüft, dass alle Kombinationen berücksichtigt werden, damit keine Ausnahmefälle übersehen werden. Dies schützt vor späteren und kostspieligen Überraschungen, beispielsweise weil nicht alle Anforderungen definiert wurden. Die Software prüft außerdem, dass jede Kombination des Problemraums genau einem Modus zugeordnet ist und es keine Überlappungen in der Definition der Modi gibt.

Schritt 3

Übergänge zwischen den Modi definieren

Im dritten Schritt wird definiert, wie das System hinsichtlich der Übergänge zwischen den Modi reagieren soll. Dazu wird in einer Tabelle oder einer grafischen Oberfläche festgelegt, welches Ereignis einen Übergang von einem Modus in einen anderen auslöst. Es kann auch festgelegt werden, dass Übergänge zwischen bestimmten Modi nicht zulässig sind. Die definierten Ereignisse werden analog zu den Modi auf Vollständigkeit, Deadlocks und weitere Eigenschaften überprüft.