Checking and Establishing Reachset Conformance in CORA 2023

Tool presentation: When formally verifying models of cyber-physical systems, it is obviously important that their verification results can be transferred to all previous observations of the modeled systems. Our tool CORA makes it possible to transfer safety properties by checking whether all measurements of the real system lie in the set of reachable outputs of the corresponding model – we call this reach set conformance checking. In addition, we provide strategies to establish reach set conformance by injecting non determinism in models. This can be seen as some form of system identification, where instead of finding the most likely parameters, we compute a set of parameter values – not only for the model dynamics but also for the set of disturbances and measurement errors – to establish reach set conformance. By replacing real measurements with simulation results from a high-fidelity model, one can also check whether a high-fidelity model conforms to a simple model. We demonstrate the usefulness of reach set conformance by several use cases.