TY - JOUR ID - deploy46 UR - http://deploy-eprints.ecs.soton.ac.uk/46/ A1 - Bendisposto, Jens A1 - Leuschel, Michael A1 - Ligot, Olivier A1 - Samia, Mireille Y1 - 2008/// N2 - The B-method, as well as its offspring Event-B, are both formal methods used for the development of critical computer systems whose correctness has to be formally established. Event-B now spurs the Rodin platform, which is based on Eclipse and can be extended via plug-ins. In this paper, we present two such plug-ins; one for animation and one for interactive proof support, called a disprover. Both plug-ins are based on the ProB tool as well as a translation of Event-B to classical B. With our new plug-ins, Rodin has now become a platform where a user can animate, prove and disprove formal models in an integrated fashion. JF - TSI TI - La validation de modèles Event-B avec le plug-in ProB pour RODIN SP - 1065 AV - public EP - 1084 ER -