Arut Prakash Kaleeswaran, Arne Nordmann, Thomas Vogel, and Lars Grunske. “Counterexample Interpretation for Contract-Based Design”. In: 7th International Symposium on Model-Based Safety and Assessment. IMBSA ’20. Springer, 2020, pp. 99–114. DOI: 10.1007/978-3-030-58920-2_7.
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.
@inproceedings{2020-IMBSA,
author = {Kaleeswaran, Arut Prakash and Nordmann, Arne and Vogel, Thomas and Grunske, Lars},
title = {Counterexample Interpretation for Contract-Based Design},
year = {2020},
booktitle = {7th International Symposium on Model-Based Safety and Assessment},
series = {IMBSA~'20},
publisher = {Springer},
pages = {99--114},
doi = {10.1007/978-3-030-58920-2_7},
}