Industrial deployment of system engineering methods providing high dependability and productivity


La validation de modèles Event-B avec le plug-in ProB pour RODIN

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.

PDF - Accepted Version


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.

Item Type:Article
Subjects:Tool developments > Model checking
Tool developments
Tool developments > Provers
ID Code:46
Deposited By:Prof Michael Leuschel
Deposited On:04 Nov 2008 09:16
Last Modified:19 Apr 2010 16:05

Repository Staff Only: item control page

Deploy-Project - All right reserved