Executable implementations are ultimately the only dependable representations of a software component's behavior. Incorporating such a component in a rigorous model-based development of reactive systems poses challenges since a formal contract over its behaviors will have to be crafted for system verification. Simply hypothesizing a contract based on informal descriptions of the component is problematic: if it is too weak, we may fail in verifying valid system-level contracts; if it is too strong or simply erroneous, the system may fail in operation. Thus, establishing a valid and strong enough contract is crucially important.In this paper, we propose to repair the invalid hypothesized contract by replacing one or more of its sub-expressions with newly composed expressions, such that the new contract holds over the implementation. To this effect, we present a novel, sound, semantically minimal, and under reasonable assumptions terminating, and complete counterexample-guided general-purpose algorithm for repairing contracts. We implemented and evaluated our technique on more than 4,000 mutants with various complexities generated from 29 valid contracts for 4 non-trivial Java reactive components. Results show a successful repair rate of 81.51%, with 20.72% of the repairs matching the manually written contracts and 60.79% of the repairs describing non-trivial valid contracts.
|Original language||English (US)|
|Title of host publication||Proceedings - IEEE/ACM 10th International Conference on Formal Methods in Software Engineering, FormaliSE 2022|
|Publisher||Institute of Electrical and Electronics Engineers Inc.|
|Number of pages||12|
|State||Published - 2022|
|Event||10th IEEE/ACM International Conference on Formal Methods in Software Engineering, FormaliSE 2022 - Pittsburgh, United States|
Duration: May 18 2022 → May 19 2022
|Name||Proceedings - IEEE/ACM 10th International Conference on Formal Methods in Software Engineering, FormaliSE 2022|
|Conference||10th IEEE/ACM International Conference on Formal Methods in Software Engineering, FormaliSE 2022|
|Period||5/18/22 → 5/19/22|
Bibliographical noteFunding Information:
Also, the research described in this paper has been supported in part by the National Science Foundation under grant 1563920.
© 2022 ACM.