Integrating Model Checking into a Live Modeling Environment

Live modeling is the ability to change an executable model at runtime, and without having to restart its execution. Sometimes this 'breaks' the ongoing execution, but in many cases, it does not have to. In earlier work, we reduced this problem to detecting fine-grained read/write conflicts between the recorded history of edit operations (created by the user) and execution steps (created by the interpreter). In this paper, we extend our approach by adding the ability to perform model checking during live modeling sessions. We motivate that this further enhances the live modeling experience, producing counter-examples or 'witness traces' relative to the current execution state, as a possible 'future', integrated with the execution and edit history, minimizing the mental gap. The model checker itself is generic, and uses (via an adapter) the language's existing interpreter. This way, we could implement this paper's running example in a working prototype with relatively little effort.