Faculté informatique et communications IC, Département d'informatique (Laboratoire de génie logiciel LGL)

Stepwise refinement of formal specifications based on logical formulae : from CO-OPN/2 specifications to Java programs

Di Marzo Serugendo, Giovanna ; Strohmeier, Alfred (Dir.)

Thèse sciences Ecole polytechnique fédérale de Lausanne EPFL : 1999 ; no 1931.

Ajouter à la liste personnelle
    Summary
    One of the steps making it possible to increase the quality and the reliability of the software executing on distributed systems consists of the use of methods of software engineering that are known as formal. The majority of the formal methods currently existing correspond in fact more to formal specifications languages than to methods themselves. This is due to the fact that the two fundamental aspects which are: the logic of use of the language and the coverage of the software life cycle are not, for the majority, defined. The development by stepwise refinement is one of the means making it possible to define these two aspects. This thesis aims to the definition of the concepts of refinement and implementation of model-oriented formal specifications. It brings a methodological base making it possible to use such a specifications language during a development by stepwise refinements and during the implementation stage. This thesis defines, initially, a theoretical framework for the refinement and the implementation of formal specifications. The main idea consists in associating a contract with each specification. A contract explicitly represents the whole of the properties of the specification which it is necessary to preserve at the time of a refinement of this specification. To show that a concrete specification refines some abstract specification, it is then a matter of showing that the contract of the concrete specification is sufficient to ensure the properties corresponding to the contract of the abstract specification. The second part of this thesis consists in applying this theoretical framework in the context of the CO-OPN/2 language. CO-OPN/2 is an object-oriented formal specifications language founded on algebraic specifications and Petri nets. Thus, definitions of the concepts of contracts, refinement and implementation are proposed for this language. The contracts are expressed using the Hennessy-Milner temporal logic (HML). This logic is used in the theory of test provided with language CO-OPN/2. Thus, the verification of the contractual properties, as well as the verification of the stages of refinement are facilitated. Refinement and implementation are controlled semantically by the satisfaction of the contracts; syntactically, a renaming is authorised. We specifically study the implementation using the Java programming language. We show how to specify classes of the Java programming language using language CO-OPN/2, so that the last stage of the process of refinement leads to a specification entirely built using CO-OPN/2 components specifying Java classes. The stage of implementation in the Java language itself is thus facilitated. The third part of this thesis shows how it is possible to practically verify that a CO-OPN/2 specification satisfies its own contract, that a stage of refinement is correctly carried out, and finally that the stage of implementation is correctly performed. These verifications are carried out using the theory of the test provided with language CO-OPN/2. Finally, the last part of this thesis illustrates the cogency of this approach by applying it to a complete and detailed case study. A distributed Java application is developped according to the method introduced for the CO-OPN/2 language. Refinement is guided mainly by the satisfaction of functional requirements and by constraints of design integrating the concept of client/server architecture. Lastly, the stages chosen in the refinement process of this development make it possible to study aspects specific to distributed applications, and to propose generic schemas for the design of such applications.
    Résumé
    Une des démarches permettant d'augmenter la qualité et la fiabilité des logiciels s'exécutant sur des systèmes répartis consiste en l'utilisation de méthodes de génie logiciel dites formelles. La majorité des méthodes formelles actuellement existantes correspondent en fait plus à des langages de spécifications formelles qu'à des méthodes proprement dites. Ceci provient du fait que les deux aspects fondamentaux que sont: la logique d'utilisation du langage et la couverture du cycle de vie du logiciel ne sont, pour la plupart, pas définis. Le développement par raffinements successifs est l'un des moyens permettant de définir ces deux aspects. Cette thèse vise à la définition des notions de raffinement et d'implantation de spécifications formelles orientées-modèles. Elle apporte par là-même une base méthodologique permettant d'utiliser un tel langage de spécifications lors d'un développement par raffinements successifs et lors de l'étape d'implantation. Cette thèse définit, dans un premier temps, un cadre théorique pour le raffinement et l'implantation de spécification formelles orientées-modèles. L'idée principale consiste à associer un contrat à chaque spécification. Un contrat représente explicitement l'ensemble des propriétés de la spécification qu'il est nécessaire de préserver lors d'un raffinement de cette spécification. Pour montrer qu'une spécification concrète raffine une spécification plus abstraite, il s'agit alors de montrer que le contrat de la spécification concrète est suffisant pour assurer les propriétés correspondant au contrat de la spécification abstraite. La seconde partie de cette thèse consiste à appliquer ce cadre théorique dans le contexte du langage CO-OPN/2. CO-OPN/2 est un langage de spécifications formelles orienté-objet, fondé sur les réseaux de Petri et les spécifications algébriques. Il est donc proposé pour ce langage, une définition des notions de contrats, de raffinement et d'implantation. Les contrats sont exprimés à l'aide de la logique temporelle de Hennessy-Milner (HML). Cette logique facilite la vérification des propriétés contractuelles, ainsi que la vérification des étapes de raffinement. Le raffinement et l'implantation sont contrôlés sémantiquement par la satisfaction des contrats; syntaxiquement, un renommage est autorisé. L'implantation utilisant le langage de programmation Java a été plus particulièrement étudiée. Il est montré comment spécifier des classes du langage de programmation Java à l'aide du langage CO-OPN/2, afin que la dernière étape du processus de raffinement conduise à une spécification entièrement construite à l'aide de composants CO-OPN/2 spécifiant des classes Java. L'étape d'implantation dans le langage Java lui-même en est ainsi facilitée. La troisième partie de cette thèse montre comment il est possible de vérifier pratiquement qu'une spécification CO-OPN/2 satisfait son propre contrat, qu'une étape de raffinement est correctement effectuée, et enfin que l'étape d'implantation est correctement réalisée. Ces vérifications s'effectuent à l'aide de la théorie du test fournie avec le langage CO-OPN/2. Finalement, la dernière partie de cette thèse illustre le bien-fondé de cette approche en l'appliquant sur une étude de cas complète et détaillée. Une application répartie Java est développée selon la méthode introduite pour le langage CO-OPN/2. Le raffinement est guidé principalement par la satisfaction de charges fonctionnelles et par des contraintes de conception intégrant la notion d'architecture client/serveur. Enfin, les étapes choisies lors du processus de raffinement de ce développement permettent d'étudier certains aspects spécifiques aux applications réparties, et de proposer des schémas génériques pour la conception de telles applications.