Résumé : Dans le cadre du développement prouvé et incrémental de systèmes informatiques, nous nous intéressons à des systèmes transactionnels présents dans les échanges bancaires comme Mondex. Nous étudions la combinaison de modèles Event B comme un modèle du Mondex et un modèle de protocoles cryptologiques afin d'obtenir un système plus robuste aux attaques. Puis, nous montrons sur quels principes est fondée cette combinaison et nous montrons dans quelles mesures elle peut simplifier la tâche de modélisation prouvée et incrémentale.
https://hal.inria.fr/inria-00426405
Contributor : Nazim Benaissa
<>
Submitted on : Monday, October 26, 2009 - 11:21:20 AM
Last modification on : Thursday, September 19, 2019 - 5:00:14 PM
Long-term archiving on : Tuesday, October 16, 2012 - 12:40:22 PM
Nazim Benaissa, Dominique Méry. Développement combiné et prouvé de systèmes transactionnels cryptologiques. Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL 2009, Jan 2009, Toulouse, France. ⟨inria-00426405⟩
