Counterexample-guided inductive repair of reactive contracts
Soha Hussein, Sanjai Rayadurgam, Stephen McCamant, Vaibhav Sharma, Mats P. E. Heimdahl · 2022
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.