Abstract
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. |
Pages | 46-57 |
Number of pages | 12 |
ISBN (Electronic) | 9781450392877 |
DOIs | |
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 |
Publication series
Name | Proceedings - IEEE/ACM 10th International Conference on Formal Methods in Software Engineering, FormaliSE 2022 |
---|
Conference
Conference | 10th IEEE/ACM International Conference on Formal Methods in Software Engineering, FormaliSE 2022 |
---|---|
Country/Territory | United States |
City | Pittsburgh |
Period | 5/18/22 → 5/19/22 |
Bibliographical note
Funding Information:Also, the research described in this paper has been supported in part by the National Science Foundation under grant 1563920.
Publisher Copyright:
© 2022 ACM.