An Approach to Integrate Formal Validation in an OO Life-cycle of Protocols

Claude Jard 1 Jean-Marc Jézéquel 1 Laurence Nedelka 1
1 PAMPA - Models and Tools for Programming Distributed Parallel Architectures
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, INRIA Rennes
Abstract : Despite excellent results on pilot projects, formal validation based on standard Formal Description Techniques (FDTs) never really catch up in the industry. We claim that this is mainly due to standard FDTs lack of support for the modern software development methods and life-cycles needed in the construction and maintenance of open distributed systems. We propose to go the other way round, that is to integrate formal validation technology within well established object-oriented (OO) development methods. Building on the intuition that a universal language taking into account all the possible semantics aspects of parallelism and communication is a holy grail, we propose to rely on an open (but simpler) OO language to build dedicated frameworks. Such frameworks can be specialized toward classes of distributed applications, and integrate formal validation tools. We illustrate our approach using the famous alternating bit protocol example. We investigate on this example how a continuous validation framework could be set up to go smoothly from the OO analysis to the OO implementation of a validated distributed system.
Type de document :
[Research Report] RR-2808, INRIA. 1996
Liste complète des métadonnées
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 13:59:32
Dernière modification le : mercredi 16 mai 2018 - 11:23:04
Document(s) archivé(s) le : lundi 5 avril 2010 - 00:01:00



  • HAL Id : inria-00073884, version 1


Claude Jard, Jean-Marc Jézéquel, Laurence Nedelka. An Approach to Integrate Formal Validation in an OO Life-cycle of Protocols. [Research Report] RR-2808, INRIA. 1996. 〈inria-00073884〉



Consultations de la notice


Téléchargements de fichiers