Reachset conformance testing of hybrid automata

Industrial-sized hybrid systems are typically not amenable to formal veri-cation techniques. For this reason, a common approach is to formally verify abstractions of (parts of) the original system. However, we need to show that this abstrac-tion conforms to the actual system implementation including its physical dynamics. In particular, veri-ed properties of the abstract system need to transfer to the implementation. To this end, we introduce a formal conformance relation, called reachset conformance, which guarantees transference of safety properties, while being a weaker relation than the existing trace inclusion conformance. Based on this formal relation, we present a conformance testing method which allows us to tune the trade-off between accuracy and com-putational load. Additionally, we present a test selection algorithm that uses a coverage measure to reduce the num-ber of test cases for conformance testing. We experimentally show the benefits of our novel techniques based on an exam-ple from autonomous driving.