ProB

ProB: an automated analysis toolset for the B method. We present ProB, a validation toolset for the B method. ProB’s automated animation facilities allow users to gain confidence in their specifications. ProB also contains a model checker and a refinement checker, both of which can be used to detect various errors in B specifications. We describe the underlying methodology of ProB, and present the important aspects of the implementation. We also present empirical evaluations as well as several case studies, highlighting that ProB enables users to uncover errors that are not easily discovered by existing tools.


References in zbMATH (referenced in 67 articles )

Showing results 21 to 40 of 67.
Sorted by year (citations)
  1. Mota, A.; Farias, A.; Woodcock, J.; Larsen, P. G.: Model checking CML: tool development and industrial applications (2015) ioport
  2. Sulskus, Gintautas; Poppleton, Michael; Rezazadeh, Abdolbaghi: An interval-based approach to modelling time in Event-B (2015) ioport
  3. Vu, Dieu-Huong; Chiba, Yuki; Yatake, Kenro; Aoki, Toshiaki: Checking the conformance of a Promela design to its formal specification in Event-B (2015)
  4. Li, Yi; Dong, Jin Song; Sun, Jing; Liu, Yang; Sun, Jun: Model checking approach to automated planning (2014)
  5. Llano, Maria Teresa; Ireland, Andrew; Pease, Alison: Discovery of invariants through automated theory formation (2014) ioport
  6. Hallerstede, Stefan; Leuschel, Michael; Plagge, Daniel: Validation of formal models by refinement animation (2013)
  7. Hoang, Thai Son: Security invariants in discrete transition systems (2013)
  8. Jones, Cliff B.; Freitas, Leo; Velykis, Andrius: Ours \textitisto reason why (2013)
  9. Perna, Juan I.; George, Chris: Model checking RAISE applicative specifications (2013)
  10. Barbosa, Haniel; Déharbe, David: An approach using the B method to formal verification of PLC programs in an industrial setting (2012) ioport
  11. Hallerstede, Stefan; Leuschel, Michael: Experiments in program verification using Event-B (2012)
  12. Leino, K. Rustan M.; Yessenov, Kuat: Stepwise refinement of heap-manipulating code in Chalice (2012)
  13. Leuschel, Michael; Llorens, Marisa; Oliver, Javier; Silva, Josep; Tamarit, Salvador: Static slicing of explicitly synchronized languages (2012)
  14. Ndukwu, Ukachukwu: Generating counterexamples for quantitative safety specifications in probabilistic B (2012)
  15. Plagge, Daniel; Leuschel, Michael: Validating B,Z and TLA(^ + ) using ProB and Kodkod (2012) ioport
  16. Vaz, Cátia; Ferreira, Carla: On the analysis of compensation correctness (2012)
  17. Williams, David M.; de Ruiter, Joeri; Fokkink, Wan: Model checking under fairness in ProB and its application to fair exchange protocols (2012)
  18. Leuschel, Michael; Bendisposto, Jens: Directed model checking for B: an evaluation and new techniques (2011)
  19. Leuschel, Michael; Falampin, Jérôme; Fritz, Fabian; Plagge, Daniel: Automated property verification for large scale B models with ProB (2011) ioport
  20. Llorens, Marisa; Oliver, Javier; Silva, Josep; Tamarit, Salvador: Graph generation to statically represent CSP processes (2011)