Counterexample-Guided Inductive Repair of Reactive Contracts

Soha M Hussein, Sanjai Rayadurgam, Stephen McCamant, Vaibhav B Sharma, Mats Heimdahl

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

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 languageEnglish (US)
Title of host publicationProceedings - IEEE/ACM 10th International Conference on Formal Methods in Software Engineering, FormaliSE 2022
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages46-57
Number of pages12
ISBN (Electronic)9781450392877
DOIs
StatePublished - 2022
Event10th IEEE/ACM International Conference on Formal Methods in Software Engineering, FormaliSE 2022 - Pittsburgh, United States
Duration: May 18 2022May 19 2022

Publication series

NameProceedings - IEEE/ACM 10th International Conference on Formal Methods in Software Engineering, FormaliSE 2022

Conference

Conference10th IEEE/ACM International Conference on Formal Methods in Software Engineering, FormaliSE 2022
Country/TerritoryUnited States
CityPittsburgh
Period5/18/225/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.

Fingerprint

Dive into the research topics of 'Counterexample-Guided Inductive Repair of Reactive Contracts'. Together they form a unique fingerprint.

Cite this