Timed-pNets: A Communication Behavioural Semantic Model for Distributed Systems (extended version)

This paper presents an approach to build a communication behavioural semantic model for heterogeneous distributed systems that include synchronous and asynchronous communications. Since each node of such system has its own physical clock, it brings the challenges of correctly specifying the system's time constraints. Based on the logical clocks proposed by Lamport and CCSL proposed by Aoste team in INRIA as well as pNets from Oasis team in INRIA, we develop timed-pNets to model communication behaviour for distributed systems. Timed-pNets are tree style hierarchical structures. Each node is associated with a timed specification which consists of a set of logical clocks and some relations on clocks. The leaves are represented by timed-pLTSs and non-leaf nodes are represented by timed-pNets including some holes which are filled by leaves or non-leaf nodes. Both timed-pLTSs and timed-pNets node can be translated to timed specifications. All these notions and methods are illustrated on a simple use-case of car insertion from the area of Intelligent Transportation Systems (ITS) and then TimeSquare tool is used to simulate and check the validity of our model.Cet article présente une nouvelle approche pour définir un modéle sémantique comportemental pour des systémes distribués comportant des communications aussi bien synchrones qu'asynchrones. Chaque site dans ce genre de systéme ayant sa propre horloge, définir correctement les contraintes temporelles globales du systéme est un défi. Á partir des concepts d'horloges virtuelles de Lamport, du langage CCSL introduit par l'équipe AOSTE d'INRIA, et du modéle pNets de l'équipe OASIS, nous développons notre modéle Timed-pNets pour exprimer les comportements et la communication de ces systémes distribués. Les Timed-pNets sont des structures hiérarchiques arborescentes. Á chaque noeud est associée une {\sl spécification temporelle} composée d'un ensemble d'horloges et de relations entre ces horloges. Les noeuds feuilles sont representés par des Timed-pLTSs (systémes de transitions paramétrés temporisés), et les autres noeuds sont soit recursivement des Timed-pNets, soit des trous (Holes) destinés á être remplis ultérieurement par des Timed-pNets. Nous définissons des algorithmes permettant de synthétiser la spécification temporelle des Timed-pLTSs et des Timed-pNets. Toutes ces notions sont illustrées sur un exemple de conduite automatisée de véhicules, issue du monde des systémes de transport intelligents (ITS); finalement nous utilisons le logiciel TimeSquare pour simuler notre modéle et en vérifier la validit