Timed-pNets： a communication behavioural semantic model for distributed systems  

作　　者：Yanwen CHEN Yixiang CHEN Eric MADELAINE 

机构地区：[1]MoE Engineering Research Center for Software/Hardware Co-design Technology and Application, Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China [2]INRIA Sophia Antipolis Mediterannee, Sophia Antipolis 06902, France, [3]University of Nice Sophia Antipolis, CNRS, Sophia Antipolis 06900, France

出　　处：《Frontiers of Computer Science》2015年第1期87-110,共24页中国计算机科学前沿（英文版）

基　　金：This work was partially funded by the INRIA Associated Team DAESD between INRIA and ECNU; by the National Basic Research Program of China （973 Program） （2011CB302802）; by the National Natural Science Foundation of China （Grant Nos. 61321064 and 61370100）; by Shanghai Knowledge Service Platform Project （ZF1213）. We give great thanks to Frederic Mallet and Jalien Deantoni who took time to discuss with us and gave us bunches of advices. We are also indebted to the anonymous referees for their suggested improvements.

摘　　要：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 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 behaviours 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. Non-leaf nodes （called timed-pNets nodes） are synchronisation devices that synchronize the behaviours of subnets （these subnets can be leaves or non-leaf nodes）. Both timed-pLTSs and timed-pNets nodes 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）. In the end the TimeSquare tool is used to simulate and check the validity of our model.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 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 behaviours 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. Non-leaf nodes （called timed-pNets nodes） are synchronisation devices that synchronize the behaviours of subnets （these subnets can be leaves or non-leaf nodes）. Both timed-pLTSs and timed-pNets nodes 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）. In the end the TimeSquare tool is used to simulate and check the validity of our model.

关 键 词：ITS logical time formal method timed specification synchronous and asynchronous communication 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构] TP311.5[自动化与计算机技术—计算机科学与技术]