A Timed Communication Behaviour Model For Distributed Systems

With the development of the Internet, CPSs (Cyber Physical Systems) become a hot topic. A typical example are ITSs (Intelligent Transportation Systems), where communication is a critical part. In this kind of system, vehicles can communicate with the infrastructure (V2I) to inform their ex-istence for safety checking; and vehicles can also communicate between each other to improve the efficiency of traffic and avoid accidents.The real-time communication in the system is a critical aspect. This thesis presents a novel timed model called timed-pNets for modeling and verifying the timed communication behaviours for distributed systems. Since the nodes in distributed systems have no common physical clock, this brings the challenge of correctly specifying the system time constraints. Timed-pNets build the time model on top of logical clocks such that the time of this model does not rely on a common physical clock.The main contribution of the thesis are as follows:· A formalism named Timed-pNets that is based on tree style hierarchi-cal structures. The leaves of the structures are represented by timed Parametrized Label Transition Systems (timed-pLTSs). Non-leaf nodes (called timed-pNets nodes) are synchronisation devices that synchro-nize the behaviours of subnets (these subnets can be leaves or non-leaf nodes). Moreover, we discuss the compatibility and delay properties of the model.· Timed specifications, are at the core of this model and are designed to specify the system behaviours including synchronous and asynchronous communications. They consist of sets of logical clocks and some re-lations on these clocks. Moreover, we propose the concept of clock partition and clock union to simplify the timed specifications, and in-vestigate the clock relations on clock partitions.· Algorithms design for the translation of timed-pLTS and timed-pNets to timed specifications. Thanks to the timed specification. timed-pNets are able to model systems in a flexible way:from bottom to up, start-ing with detailed timed-pLTSs and assembling them in a compatible way; or from top to down, constructing timed specifications for ab-stract timed-pNets, using their timed specifications as hypotheses in an assume-guarantee style, and providing later some specific (compat-ible) implementations for these holes in various contexts.· A discussion on time bound analysis, safety and latency properties based on the analysis of the relations conflicts between system logical clocks. We take a simple case of car insertion from the area of Intelligent Transportation Systems (ITS) as an example to demonstrate the use of the timed-pNets model. The TimeSquare tool is used to perform a logical simulation and check the validity of our model.