ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne
Autres revues >>

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 27/8 - 2008  - pp.1065-1084  - doi:10.3166/tsi.27.1065-1084
TITRE
La validation de modèles Event-B avec le plug-in ProB pour RODIN

RÉSUMÉ
La méthode B, ainsi que sa progéniture Event-B, sont des méthodes formelles utilisées pour le développement de systèmes informatiques dont l'exactitude doit être formellement établie. Un grand atout d'Event-B est la plate-forme RODIN, qui est basée sur Eclipse et qui peut être étendue à l'aide de plug-ins. Dans cet article, nous présentons deux plug-ins pour RODIN : un outil d'animation ainsi qu'un outil d'aide à la preuve interactive, appelé un contre-prouveur (disprover). Les deux plug-ins ont été implémentés à l'aide de l'outil PROB et d'une traduction d'Event-B vers B classique. Avec nos outils, RODIN devient donc une plate-forme où l'utilisateur peut éditer, animer, prouver et contre-prouver des modèles d'une manière intégrée.


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.


AUTEUR(S)
Jens BENDISPOSTO, Michael LEUSCHEL, o. LIGOT, m. SAMIA

MOTS-CLÉS
event-B, méthode B, model-checking, animation, preuve automatique, RODIN, PROB.

KEYWORDS
event-B, B-method, model checking, animation, automated theorem proving, RODIN, PROB.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 12.5 €
• Non abonné : 25.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (672 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier