creators_name: Bendisposto, Jens creators_name: Leuschel, Michael creators_name: Ligot, Olivier creators_name: Samia, Mireille creators_id: leuschel@cs.uni-duesseldorf.de type: article datestamp: 2008-11-04 09:16:45 lastmod: 2010-04-19 15:05:51 metadata_visibility: show title: La validation de modèles Event-B avec le plug-in ProB pour RODIN ispublished: pub subjects: deploy_tooldev_modela subjects: deploy_tooldev subjects: Proof full_text_status: public abstract: 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. date: 2008 date_type: published publication: TSI pagerange: 1065-1084 refereed: TRUE citation: Bendisposto, Jens and Leuschel, Michael and Ligot, Olivier and Samia, Mireille (2008) La validation de modèles Event-B avec le plug-in ProB pour RODIN. TSI . pp. 1065-1084. document_url: http://deploy-eprints.ecs.soton.ac.uk/46/1/afadl07_french_tsi.pdf