title: La validation de modèles Event-B avec le  plug-in ProB pour RODIN
creator: Bendisposto, Jens
creator: Leuschel, Michael
creator: Ligot, Olivier
creator: Samia, Mireille
subject: Model checking
subject: Tool developments
subject: Provers
description: 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
type: Article
type: PeerReviewed
format: application/pdf
identifier: http://deploy-eprints.ecs.soton.ac.uk/46/1/afadl07_french_tsi.pdf
identifier:   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.      
relation: http://deploy-eprints.ecs.soton.ac.uk/46/

<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>