Direkt zum Inhalt
Symbolfoto: Das AIT ist Österreichs größte außeruniversitäre Forschungseinrichtung

Laufzeitverifikation

Cyberphysische Systeme (CPS) vereinen heterogene kollaborative Komponenten, die sowohl miteinander als auch mit ihrer physischen Umgebung verbunden sind. Sie zeigen ein komplexes Verhalten, das typischerweise durch die Kombination diskreter und kontinuierlicher Dynamik geprägt ist.

Durch die enorme Komplexität von CPS-Anwendungen, wie etwa in autonomen Fahrzeugen, ist es nahezu unmöglich, das System während der Entwicklung vollständig zu verifizieren. Die Laufzeitverifikation schafft hier einen Ausweg und bietet sich als formale, jedoch skalierbare Methode zur Verifikation und Analyse an.

Die Laufzeitverifikation kann in folgenden Fällen angewendet werden:

  • Während der Ausführung realer Systeme
  • Bei der Simulation von Systemmodellen in der Designphase

Im ersten Fall wird die Laufzeitverifikation eingesetzt, um potentielle Systemabweichungen vom Nominalverhalten zu identifizieren und gegebenenfalls Korrekturmaßnahmen zu ergreifen. Im zweiten Fall bietet die Laufzeitverifikation eine rigorose Analyse des Systemverhaltens und dient damit als Ergänzung anderer formaler Verifikationsmethoden.

Die Gruppe Dependable Systems Engineering befasst sich in der Laufzeitverifikation von CPS mit den folgenden drei Themen:

  • Spezifikationssprachen zur Beschreibung allgemeiner CPS Eigenschaften
  • Neuartige Techniken zur Laufzeitverifikation und Analyse
  • Fehlererklärung und -lokalisierung

Derzeit fokussieren wir unsere Aktivitäten auf folgende Teilaspekte:

  • Entwicklung und Einsatz von Echtzeit-Monitoren
  • Predictive System Health Monitoring
  • Eigenschaftsbasierte Parameterextraktion und Messungen aus dem Verhalten
  • Trace- und Systemdiagnose
  • Laufzeitverifikation Korrektheit vs. Robustheit

 

Publikationen

  • D. Nickovic, U. Hafner, C. Reidl, T. Nguyen, et al.: Runtime Monitoring with Recovery of the SENT Communication Protocol, CAV 2017
  • D. Nickovic, A. Rodionova, E. Bartocci, R. Grosu: Temporal Logic as Filtering, HSCC 2016, S11-20
  • D. Nickovic, S. Jaksic, E. Bartocci, R. Grosu: Quantitative Monitoring of STL with Edit Distance, RV 2016, S201-218
  • D. Nickovic, T. Ferrère, O. Maler: Trace Diagnostics Using Temporal Implicants, ATVA 2015, S241-258
  • D. Nickovic, T. Ferrère, O. Maler, D. Ulus: Measuring with Timed Patterns, CAV 2015, S322-337