MBMV 2023 – Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen
All proceedings of this conference

Runtime Verification of Hybrid Systems with Affine Arithmetic Decision Diagrams

Conference: MBMV 2023 – Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen - 26. Workshop
03/23/2023 - 03/24/2023 at Freiburg

Proceedings: ITG-Fb. 309: MBMV 2023

Pages: 10Language: englishTyp: PDF

Authors:
Heermann, Hagen; Grimm, Christoph (RPTU, Kaiserslautern, Deutschland)

Abstract:
A novel approach for runtime verification of hybrid systems is presented. The approach uses Affine Arithmetic Decision Diagrams to describe and compute the reachable state space of a model of a hybrid system, and to generate monitors. The monitors can be used during runtime to check the consistency of observed signal trajectories against the possible dynamic behavior of the model. The consistency check is formulated as a linear programming problem.