HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 1:59:32 PM
Last modification on : Friday, February 4, 2022 - 3:22:29 AM
Long-term archiving on: : Monday, April 5, 2010 - 12:01:00 AM


  • 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⟩



Record views


Files downloads