A. Diagne, P..Estraillier Formal specification and design of distributed systems Les avantages de l'intégration des réseaux de Petri et des con­ cepts 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 mul­ ti-formalismes. Nous définissons une correspondance formelle en­ tre 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. To design Distributed Systems (DS), the advantages of integra­ tion 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 orient­ ed 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 Dis­ tributed Processing to a Petri net modular model. So specifica­ tion, design and validation of Distributed Systems can be consid­ ered in the OO paradigm which is most appropriate while verifica­ tion is done in the PN paradigm for better formality. The OO mod­ el we use is dedicated to design of distributed systems and sup­ port validation of the result in the earliest. The transformation into a PN model allows to undertake formal verification and simu­ lation of the design.