Reachset Conformance and Automatic Model Adaptation for Hybrid Systems

Abstract

Model-based verification uses a model to reason about the correctness of a real system. This requires the model and the system to be conformant, such that verification results on the model can be transfered to the real system. Especially for hybrid systems, which combine discrete and continuous behavior, defining and checking conformance is a difficult task. In this work, we present reachset conformance for hybrid systems that transfers safety properties from a model to the real system. We show how a model can be adapted to be conformant to measurements of a real system and demonstrate this for a real autonomous vehicle. The obtained reachset conformant model can be used for the verification of safety-critical properties, such as collision avoidance.

Keywords

• conformance
• reachability analysis
• formal verification
• hybrid systems
• automated vehicles
• uncertain systems