No edit summary |
|||
| Line 26: | Line 26: | ||
* [http://b4msecure.forge.imag.fr B4MSecure] | * [http://b4msecure.forge.imag.fr B4MSecure] | ||
== Tools == | == Related Tools == | ||
* [http://lifc.univ-fcomte.fr/~btatibouet/PERSO/JBTOOLS/InstallPlugIn/InstallPlugIn.html jbtools] | * [http://lifc.univ-fcomte.fr/~btatibouet/PERSO/JBTOOLS/InstallPlugIn/InstallPlugIn.html jbtools] | ||
* [http://www.b4free.com/ B4Free] tools for the development of B models | * [http://www.b4free.com/ B4Free] tools for the development of B models | ||
| Line 36: | Line 36: | ||
* [http://www.atelierb.eu/ Atelier B] | * [http://www.atelierb.eu/ Atelier B] | ||
* [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+] ([http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html tools for TLA+]) | * [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+] ([http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html tools for TLA+]) | ||
== 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> | |||