Pacemaker model by Mery and Singh: "ProB was very useful in the development of the pacemaker specification, and was able to animate all of our models and able to prove the absence of error (no counterex- ample exist). The ProB model checker also discovered several invariant violations, e.g., related to incorrect responses or unordered pacing and sensing activities. It was also able to discover a deadlock in two of the models, which was due to the fact that “clock counter” were not properly recycled, meaning that after a while no pacing or sensing activities occur into the system. Such kind of errors would have been more difficult to uncover with the prover of RODIN tool."