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 52 articles )

Showing results 1 to 20 of 52.
Sorted by year (citations)

1 2 3 next

  1. Graiet, Mohamed; Hamel, Lazhar; Mammar, Amel; Tata, Samir: A verification and deployment approach for elastic component-based applications (2017)
  2. Dobrikov, Ivaylo; Leuschel, Michael: Optimising the ProB model checker for B using partial order reduction (2016)
  3. Hoang, Thai Son; Schneider, Steve; Treharne, Helen; Williams, David M.: Foundations for using linear temporal logic in Event-B refinement (2016)
  4. Vekris, Dimitris; Lang, Frédéric; Dima, Catalin; Mateescu, Radu: Verification of $\mathrmEB^3$ specifications using CADP (2016)
  5. Mammar, Amel; Frappier, Marc: Proof-based verification approaches for dynamic properties: application to the information system domain (2015)
  6. Mota, A.; Farias, A.; Woodcock, J.; Larsen, P. G.: Model checking CML: tool development and industrial applications (2015) ioport
  7. Sulskus, Gintautas; Poppleton, Michael; Rezazadeh, Abdolbaghi: An interval-based approach to modelling time in Event-B (2015)
  8. Vu, Dieu-Huong; Chiba, Yuki; Yatake, Kenro; Aoki, Toshiaki: Checking the conformance of a Promela design to its formal specification in Event-B (2015)
  9. Li, Yi; Dong, Jin Song; Sun, Jing; Liu, Yang; Sun, Jun: Model checking approach to automated planning (2014)
  10. Llano, Maria Teresa; Ireland, Andrew; Pease, Alison: Discovery of invariants through automated theory formation (2014) ioport
  11. Hallerstede, Stefan; Leuschel, Michael; Plagge, Daniel: Validation of formal models by refinement animation (2013)
  12. Hoang, Thai Son: Security invariants in discrete transition systems (2013)
  13. Jones, Cliff B.; Freitas, Leo; Velykis, Andrius: Ours \itis to reason why (2013)
  14. Perna, Juan I.; George, Chris: Model checking RAISE applicative specifications (2013)
  15. Barbosa, Haniel; Déharbe, David: An approach using the B method to formal verification of PLC programs in an industrial setting (2012) ioport
  16. Hallerstede, Stefan; Leuschel, Michael: Experiments in program verification using Event-B (2012)
  17. Leino, K. Rustan M.; Yessenov, Kuat: Stepwise refinement of heap-manipulating code in Chalice (2012)
  18. Leuschel, Michael; Llorens, Marisa; Oliver, Javier; Silva, Josep; Tamarit, Salvador: Static slicing of explicitly synchronized languages (2012)
  19. Ndukwu, Ukachukwu: Generating counterexamples for quantitative safety specifications in probabilistic B (2012)
  20. Plagge, Daniel; Leuschel, Michael: Validating B,Z and TLA$^ + $ using ProB and Kodkod (2012) ioport

1 2 3 next