Counterexample Interpretation for Contract-Based Design

Abstract

Contract-based design (CBD) is an emerging paradigm for complex systems, specifying the input-output behavior of a component by defining what the component guarantees, provided its environment satisfies the given assumptions. Under certain circumstances, it is possible to verify the decomposition of contracts to conclude the correctness of the top-level system requirements. Verification is performed by using model checkers. If the decomposition of the contract is found to be incorrect, a model checker generates a counterexample. However, the challenging task is to understand the counterexample, which usually is lengthy, cryptic, and verbose. In this paper, we propose an approach to derive an understandable error explanation for counterexamples in CBD. In addition, we highlight the erroneous variables and erroneous states in the counterexample, which reduces the effort to identify errors. Therefore, our approach supports error comprehension of the original counterexample. Our approach is evaluated based on two industrial use cases, the Bosch Electronic Power Steering (EPS) and a redundant sensor system.