Interactive Model Repair by Synthesis
Published in Proceedings ABZ (International Conference on Rigorous State Based Methods), 2016
When using B or Event-B for formal specifications, model checking is often used to detect errors such as invariant violations, deadlocks or refinement errors. Errors are presented as counter-example states and traces and should help fixing the underlying bugs. We suggest automating parts of this process: Using a synthesis technique, we try to generate more permissive or restrictive guards or invariants. Furthermore, synthesized actions allow to modify the behaviour of the model. All this could be done with constant user feedback, yielding an interactive debugging aid.
Joshua Schmidt, Sebastian Krings and Michael Leuschel. (2016). "Interactive Model Repair by Synthesis" Proceedings ABZ (International Conference on Rigorous State Based Methods). https://link.springer.com/chapter/10.1007/978-3-319-33600-8_25