Interactive Model Repair by Synthesis

Abstract

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.

Publication
In Proceedings 5th International ABZ Conference ASM, Alloy, B, TLA, VDM, Z (ABZ 2016), Springer LNCS

Related