Formal specification and design of distributed systems

A. Diagne, P. Estraillier

Masi-IBP 1996/04: Rapport de Recherche Masi / Masi research reports
24 pages - Mars/March 1996 - Document en anglais.

PostScript : 14 Ko /Kb

Titre français : Spécification et Conception Formelle de Systèmes Répartis
Titre anglais : Formal specification and design of distributed systems

Résumé : Les avantages de l'intégration des réseaux de Petri et des concepts orientés objets dans le domaine de la spécification et de la conception des systemes répartis ont ete largement discutés dans la littérature. Certaines tentatives d'intégration visent à fournir une base formelle à des langages orientés objet tandis que d'autres enrichissent les réseaux de Petri avec des types de données abstraits. Dans les deux cas, l'utilisation des réseaux de Petri est explicite et le résultat diverge d'un modèle objet classique. Le but de ce travail est de proposer une approche multi-formalismes. Nous définissons une correspondance formelle entre un modèle orienté objet déduit du modèle de reference de l'ODP et un modèle de réseau de Petri modulaire. Ainsi on pourra spécifier et concevoir dans le schema objet classique, ensuite procéder a des vérifications formelles de propriétés avec le modèle réseau de Petri.

Abstract : To design Distributed Systems (DS), the advantages of integration of Petri Nets (PN) and Object Oriented (OO) concepts had been widely discussed in the literature. Some integrations are mainly concerned with providing a formal basis for object oriented languages. Others focus on combining the abstract data type of the object technology with Petri nets. In both approaches the use of Petri nets is explicit so the resulting model diverge from the classical OO technology. The aim of this work is to bridge the gap between the two paradigms by a formal transformation from a 'pure' OO model derived from the Reference Model for Open Distributed Processing to a Petri net modular model. So specification, design and validation of Distributed Systems can be considered in the OO paradigm which is most appropriate while verification is done in the PN paradigm for better formality. The OO model we use is dedicated to design of distributed systems and support validation of the result in the earliest. The transformation into a PN model allows to undertake formal verification and simulation of the design.

Mots-clés : Systèmes Répartis, Spécification, Conception, RM-ODP, Réseaux de Petri, Validation, Vérification Formelle, Simulation.

Key-words : Distributed Systems, Specification, Design, RM-ODP, Validation, Formal Verification, Simulation, Petri Nets.

Publications internes Masi 1996 / Masi research reports 1996