Département d'informatique, IC - Section d'informatique IC-SIN (Laboratoire de génie logiciel LGL)

An incremental prototyping methodology for distributed systems based on formal specifications

Hulaas, Jarle ; Strohmeier, Alfred (Dir.)

Thèse Ecole polytechnique fédérale de Lausanne EPFL : 1997 ; no 1664.

Ajouter à la liste personnelle
    Summary
    This thesis presents a new incremental prototyping methodology for formally specified distributed systems. The objective of this methodology is to fill the gap which currently exists between the phase where a specification is simulated, generally using some sequential logical inference tool, and the phase where the modeled system has a reliable, efficient and maintainable distributed implementation in a main-stream object-oriented programming language. This objective is realized by application of a methodology we call Mixed Prototyping with Object-Orientation (in short: OOMP). This is an extension of an existing approach, namely Mixed Prototyping, that we have adapted to the object-oriented paradigm, of which we exploit the flexibility and inherent capability of modeling abstract entities. The OOMP process proceeds as follows. First, the source specifications are automatically translated into a class-based object-oriented language, thus providing a portable and high-level initial implementation. The generated class hierarchy is designed so that the developer may independently derive new sub-classes in order to make the prototype more efficient or to add functionalities that could not be specified with the given formalism. This prototyping process is performed incrementally in order to safely validate the modifications against the semantics of the specification. The resulting prototype can finally be considered as the end-user implementation of the specified software. The originality of our approach is that we exploit object-oriented programming techniques in the implementation of formal specifications in order to gain flexibility in the development process. Simultaneously, the object paradigm gives the means to harness this newly acquired freedom by allowing automatic generation of test routines which verify the conformance of the hand-written code with respect to the specifications. We demonstrate the generality of our prototyping scheme by applying it to a distributed collaborative diary program within the frame of CO-OPN (Concurrent Object-Oriented Petri Nets), a very powerful specification formalism which allows expressing concurrent and non-deterministic behaviours, and which provides structuring facilities such as modularity, encapsulation and genericity. An important effort has also been accomplished in the development or adaptation of distributed algorithms for cooperative symbolic resolution. These algorithms are used in the run-time support of the generated CO-OPN prototypes.
    Résumé
    Cette thèse présente une nouvelle méthodologie de prototypage incrémental pour systèmes répartis spécifiés formellement. L’objectif de cette méthodologie est de combler le vide qui existe actuellement entre la phase où la spécification est simulée, généralement au moyen d’un outil d’inférence séquentiel, et la phase où le système modélisé possède une implémentation répartie, dans un langage de programmation à objets courant, et qui soit fiable, efficace et permettant la maintenance. Cet objectif est atteint par l’application d’une méthodologie que nous appelons le prototypage mixte à objets (sigle anglais: OOMP). Il s’agit d’une extension d’une approche existante, le prototypage mixte, que nous adaptons au paradigme objet dont nous exploitons la flexibilité et la capacité inhérente à modéliser des entités abstraites. Le processus OOMP se déroule comme suit. Premièrement, les spécifications sources sont automatiquement traduites dans un langage à objets à structure de classes, fournissant ainsi une implémentation initiale portable et de haut niveau. La hiérarchie de classes générée est conçue de manière à laisser au développeur la liberté de dériver de façon indépendante de nouvelles sous-classes afin de rendre le prototype plus efficace ou pour ajouter des fonctionnalités qui ne peuvent pas être spécifiées dans le formalisme choisi. Ce processus de prototypage est poursuivi par petits incréments, ce qui permet de valider chaque étape par rapport à la sémantique de la spécification. Le prototype résultant peut finalement être considéré comme l’implémentation définitive du logiciel spécifié. L’originalité de notre approche réside dans l’exploitation de techniques de programmation par objets pour l’implémentation de spécifications formelles afin d’augmenter la flexibilité dans le processus de développement. Simultanément, le paradigme objet donne aussi les moyens de maîtriser cette liberté nouvellement acquise en autorisant la génération automatique de routines de test qui vérifient la conformité du code écrit à la main par rapport aux spécifications. Nous démontrons la généralité de notre méthode de prototypage par son application à un programme d’agenda collaboratif réparti; cet exercice est effectué dans le cadre de CO-OPN (Concurrent Object-Oriented Petri Nets), un formalisme de spécification très puissant qui permet d’exprimer des comportements concurrents et non-déterministes, et qui fournit de riches possibilités de structuration telles que modularité, encapsulation et généricité. Un important travail a également été accompli pour développer ou adapter des algorithmes répartis pour la résolution symbolique coopérative. Ces algorithmes sont utilisés dans le support d’exécution des prototypes générés sur la base de spécifications CO-OPN.