No edit summary |
|||
| Line 39: | Line 39: | ||
== Testimonies == | == Testimonies == | ||
* [http://dl.acm.org/citation.cfm?doid=2406336.2406351 Pacemaker model by Mery and Singh]: <i>"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."</i> | * [http://dl.acm.org/citation.cfm?doid=2406336.2406351 Pacemaker model by Mery and Singh]: <i>"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."</i> | ||
* [http://www.ncl.ac.uk/computing/research/publication/197269 Safecap tool paper by Iliasov, Lopatkin and Romanovsky] <i>"One of the larger examples we have tackled is the Carlisle Citadel station with the North, South, and Caldew junctions. The modelled fragment is 2.6km long and comprises 70 train detection circuits, 63 points, 79 routes and 161 valid paths. The translation from a scanned PDF drawing and printed control tables took 45 man-hours. The verification of the topology theory constraints using ProB took just over 6 minutes on a PC with i7 3730 CPU and utilized just under 2GB of RAM. The Why3 verification of the same theory takes approximately 70 minutes. The control table theory is verified under 20 seconds by ProB and not verified completely, with the current translation of conditions, using Why3."</i> | |||