Software Requirements Engineering

Szenario-basierte, formale Anforderungsspezifikation

  • Anforderungen an kooperierende, technische Systeme (u.a. eingebettete, mechatronische und cyberphysische Systeme)
  • Anforderungen an das nachrichtenbasierte Kommunikationsverhalten
  • Inhärente Systemkomplexität erfordert separate Betrachtung einzelner Anwendungsszenarien
  • Technische Systeme unterliegen Echtzeitanforderungen
  • UML-konforme Variante von Live Sequence Charts
  • Formale und modale Semantik
  • Intuitive Anforderungsmodellierung strukturiert durch Use Cases
  • Explizite Modellierung von Annahmen an die Umwelt des zu entwickelnden Systems
  • Kontinuierliches Echtzeitmodell basierend auf Clock-Zones

Analysetechniken

  • Simulative Validierung mittels Play-out-Algorithmus
  • Nachvollziehen des Gesamtverhaltens, welches aus einzelnen Szenarien resultiert
  • Automatische Synthese von zustandsbasierten Controllern aus MSDs
  • Anforderungen sind konsistent und realisierbar, wenn ein Controller aus MSDs synthetisiert werden kann
  • Synthese eines Gegenbeispiels im Falle von Inkonsistenzen

Software Modellierung

Koordination durch Kommunikation

  • Koordinationssrollen
  • Verhalten
  • Quality of Service

Struktur

  • Ein- und ausgehende Nachrichten
  • Ein- und ausgehende Signale
  • Horizontale Komposition
  • Vertikale Komposition
  • Flexible Kardinalitäten
  • Typsichere Verbindungen

Verhalten

  • Verfeinerung von Protokollverhalten
  • Automatische Transformation von Rollen- zu Portverhalten
  • Manuelle Verfeinerung
  • Automatische Verfeinerungsüberprüfungen
  • Echtzeitbehaftete Zustandsmaschinen
  • Komposition von Portverhalten
  • Setzen und Lesen von Signalwerten
  • Formale Semantik
  • Formale Action Language

Formale Verifikation

Domänenspezifische Formale Anforderungsspezifikation mit MechatronicUML Timed Computation Tree Logic (MTCTL)

  • Code-Vervollständigung
  • Live Überprüfung der Syntax
  • Sinnvolle Fehlermeldungen
  • Eine Verklemmung wird niemals auftreten.
  • Alle Zustände / Transitionen sind erreichbar.
  • Alle Nachrichten können ihren Puffer erreichen.
  • ...
  • Vollständige Englische Sätze statt komplizierte Ausdrücke
  • Erhöht die Nachvollziehbarkeit
  • Erlaubt Requirements Experten die Eigenschaften zu verstehen

Domänenspezifisches Model Checking mit dem Uppaal Model Checker

  • Mehrstufige semantikerhaltende Transformationen
  • Übersetzung von hierachischen Automaten in flache Automaten
  • Übersetzung von domänenspezifischen Verifikationseigenschaften
  • Automatische Abbildung von Konnektoren, Nachrichtenpuffern und QoS-Eigenschaften
  • Nachvollziehbarer domänenspezifischer Trace
  • Anzeige von Uhrenwerte und Variablenwerte
  • Anzeige des Zustands der Nachrichtenpuffer und des Konnektors

Model-in-the-Loop Simulation mit COTS-Werkzeugen

MATLAB Simulink / Stateflow

  • Debuggbare Simulation in Simulink
  • Automatische Generierung des Netzwerklayers
  • Abbildung des zustandbasierten Verhaltens auf Stateflow Modelle

Modelica in Dymola

  • StateGraph2 Erweiterung
  • Freie Modelica Lizenz
  • Asynchrone Nachrichten und Puffer
  • Erweiterte Zeitkonstrukture
  • Modelica Library Award (2012)
  • Layouting auf Basis von Graphviz
  • Abbildung auf StateGraph2 und Real-Time Coordination Bibliothekselemente

Hardware Modellieren

Hardware Ressourcen

  • Komposition Atomarer Ressourcen
  • Speicher und Prozessoren
  • Netzwerkprotokolle
  • Kommunikationsschnittstellen

Hardware Plattform

  • Komposition von existierenden ECUs
  • Komposition von Plattformen
  • Wiederverwendung
  • Punkt-zu-Punkt Netzwerke
  • Kommunikationsbusse

Deployment

Design-Space Explorierung

  • OCL-basiert
  • Direkter Modellzugriff
  • Einbindung von wiederverwendbaren Bibliotheken
  • Flexibler Evaluierungskontext
  • Einzelne Queryausführung
  • Abbildung auf ein Modell linearer Gleichungen (ILP)
  • Alternative Solver
  • LPSolve
  • OPT4J

Code-Generierung

  • Komponenten
  • Real-Time Statecharts
  • Zugriff aus dem Modell auf native Softwarebibliotheken
  • Container
  • Lifecycle Handline
  • DDS Middleware Adapter
  • Aktorik- / Sensorikzugriff
  • Arduino (.ino)
  • ANSI C99 für x64 und x86 (.c + makefile)
  • nxtOSEK für Lego Mindstorms (.oil + c + makefile)

Rekonfiguration

Rekonfigurierbare Komponenten

Rekonfigurationsverhalten

  • Formale Spezifikation
  • Atomarität / Abgeschlossenheit
  • Konsitenzerhaltung
  • Isolation