Yanwen Chen
email: yxchen@sei.ecnu.edu.cn

Yixiang Chen

Eric Madelaine

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

Keywords: ITS, logical time, formal method, timed specification, synchronous and asynchronous communication

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.

Introduction

Heterogeneous distributed systems, as targeted in this paper, can be characterized by the fact that the processors are spatially separated and that a common time base does not exist. Distinct processes in such systems communicate with each other by exchanging messages with unpredictable (but nonzero) transmission delays. Intelligent transportation system (ITS) is one typical application in this area. It consists of distributed vehicles which are equipped with their own independent clocks. Despite each vehicle has a common time base (e.g. local physical clock), there is no global physical clock shared by these vehicles. In such a context, it is impossible to build time constraints (e.g. action α from process A and action β from process B happens at the same time) since the processes have no consistent view of the time.

In this paper, we propose a timed model that is able to specify time constrains based on logical time. It has been proven that logical time brings benefits to several domains. It was first introduced by Lamport to represent the execution of distributed systems [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF]. Then it was extended and used in distributed systems to check the communication and causality path correctness [START_REF] Fidge | Logical time in distributed computing systems[END_REF]. Logical time has also been intensively used in synchronous languages [START_REF] Berry | The foundations of esterel[END_REF][START_REF] Benveniste | Synchronous programming with events and relations: the signal language and its semantics[END_REF] for its multiform nature. The multiform nature of logical time consists in the ability to use any repetitive event as a reference for the other ones. It is then possible to express temporal properties between various references. In the synchronous domain it has been proven to be adaptable to any level of description, from very flexible causal time descriptions to very precise scheduling descriptions [START_REF] Boussinot | The esterel language[END_REF]. Logical time can be multiform, a global partial order built from local total orders of clocks. Inspired by the CCSL model [START_REF] André | Syntax and Semantics of the Clock Constraint Specification Language (CCSL)[END_REF], we design clock relations to specify the systems logical time constraints. The logical time constraints in this paper do not rely on global physical clocks. We consider the constraints as dependency relations. For example, a coincidence relation in this paper forces two actions to occur simultaneously (e.g. they wait for the same data to be ready to trigger the execution of the two actions), which means that one action (e.g. "α") can occur if and only if another action (e.g. "β") occurs. Thus the term "simultaneous" (or "at the same time") in this paper does not mean the two actions really occur at the same timestamp (e.g. at 20:30 of the same global physical clock), but they must logically coincide (i.e. α occurs if and only if β occurs, but the timestamps of them may not be the same). So our model is a logical constrained model that is expressed by a set of logical clocks and clock constraints. In a heterogeneous distributed system design cycle, from an initial set of abstract time relations, and through architecture and platform-dependent design decisions, time refinement steps take place which solve in part the constraints between clocks, committing to schedule and placement decisions. The final version should be totally ordered, and then subject to physical timing verifications and to physical constraints.

Our model is based on pNets (parametrized networks of synchronized automata) [START_REF] Barros | Behavioural models for distributed Fractal components[END_REF], an expressive and flexible semantic model for the modeling and verification of (untimed) distributed systems. The pNet model describes the behaviours of concurrent systems in terms of value-passing labelled transition systems (LTSs), and expresses communications and synchronisation with synchronisation vectors (originating in [START_REF] Arnold | Finite Transition Systems: Semantics of Communicating Systems[END_REF]). It allows to model a large variety of synchronisation mechanisms and has been traditionally used for systems of either synchronously or asynchronously communicating objects, and of distributed components [START_REF] Barros | Behavioural models for distributed Fractal components[END_REF]. The flexibility of the synchronisation vector mechanism naturally provides descriptions of heterogeneous systems, from point-to-point or multipoint synchronisation, to sophisticated asynchronous queuing policies. Parametrization and hierarchy also make pNet models compact, and close to the program structure, and as a consequence easy to generate in a compositional way [START_REF] Ameur-Boulifa | Behavioural Semantics for Asynchronous Components[END_REF]. All these advantages attracted us to choose it for modelling the systems. However, pNets have no mechanism to describe time constraints neither to explicitly define asynchronous communication behaviours. We propose a novel timed model called timed-pNets by introducing timed specifications into pNets. The timed specifications represent system logical clocks and their relations so that the system timerelated behaviours can be specified.

In recent work about ITS, or more generally on cyberphysical systems (CPS), people use models with continuous time, that is required for expressing the system physical behaviour evolution and control. In this paper, we concentrate on abstract models, that are appropriate to reason about the communications, synchronisation, and overall timing constraints of heterogeneous systems. We assume that in our model physical signals can be well sampled and transformed to digital signals. Therefore, even though we do not build continuous time model for the physical world, we do not isolate our model from it. Our model is capable to monitor and control physical behaviours by taking samples from the physical world.

In our previous work [START_REF] Chen | Timed-pNets: a formal communication behavior model for real-time cps systems[END_REF] we proposed the first version of timed-pNets, including the notion of logical clocks directly imported from CCSL. A set of clock constraints related to the logical clocks were built to describe the system casual relations. We also represented a simple use-case inspired from ITS systems, and illustrated the simulation results with execution traces by the TimeSquare tool [START_REF] Deantoni | TimeSquare: Treat your models with logical time[END_REF]. However, this model was not sufficient to build hierarchical timed specifications starting from timed-pLTSs.

In this paper, we enhance the compositional aspects of our specification methodology: a system is modelled as a hierarchy of timed-pNets as shown in Fig. 1, where leaves are timed-pLTSs (i.e. finite state machines with logical clocks on the transitions), and nodes are synchronisation devices. Products between subnets can be synchronous (modelling local components sharing synchronous clocks), or involve asynchronous communications between unrelated events, that we model as channels. From such a hierarchical model, we propose the proce-dures as follows:

• At the bottom level, analyzing timed-pLTSs, and building the timed specifications (sets of clocks and clock relations) to specify the temporal behaviours,

• For each timed-pNet node, building an abstract timed specification (= at level N), from its lower-level timed specifications (level N-1).

One important point is that timed specifications (TSs) are logical characterizations, that can be either provided by the application designers, or computed from the model. The consequence is that the procedures above can be used arbitrarily in a bottom-up fashion, starting with detailed timed-pLTSs and assembling them in a compatible way; or in a top-down fashion, constructing TSs for abstract timed-pNets, using their holes TSs as hypotheses in an assume-guarantee style, and providing later some specific (compatible) implementations for these holes in various contexts.

At each level, we are able to use the TimeSquare tool [START_REF] Deantoni | TimeSquare: Treat your models with logical time[END_REF] to simulate the possible executions of timed specifications.

The remainder of the paper is organized as follows. Section 2 represents the technical background including the definitions of pLTS and pNets. Section 3 describes the meaning of timed specifications including the formal definitions of timed-actions, logical clocks and their relations. Then we give the definition of timed-pLTSs in Section 4. In Section 5 we discuss how to build timed-pNets. The issue of checking the compatibility of timed-pNets is discussed in Section 6. The procedures of generating timed specifications from timed-pLTSs and timed-pNets are presented respectively in Sections 7 and 8. In Section 9 we discuss how to build multilayers timed-pNets systems. Then in Section 10 we represent the simulations by using the TimeSquare tool. Related works are listed in Section 11. Finally, we summarize the current results and outline future work.

Technical background

The pNets model [START_REF] Barros | Behavioural models for distributed Fractal components[END_REF] is a formalism to represent the behaviours of distributed applications in terms of value-passing labelled transition systems (LTSs) [START_REF] Milner | Communicating and Mobile Systems: the π-Calculus[END_REF]. The behaviours are modelled hierarchically by composition of classical LTSs [START_REF] Milner | Communication and Concurrency[END_REF] using a variant of synchronisation vectors [START_REF] Arnold | Finite Transition Systems: Semantics of Communicating Systems[END_REF]. To encode both families of processes and data value passing communications, LTSs and synchronisation vectors are enriched with parameters [START_REF] Cansado | Specification and verification for grid component-based applications: from models to tools[END_REF] that are used as communication arguments, in state definitions, and in synchronisation operators. This en-ables compact and generic description of parametrized and dynamic topologies. In the following we recall definitions of pLTS and pNets [START_REF] Barros | Behavioural models for distributed Fractal components[END_REF]. We start by giving the notion of parametrized actions that are basic elements for pLTSs. Definition (parametrized actions) Let P be a set of names, L A,P a term algebra built over P, including at least a distinguished sort A for actions, and a constant action τ. We call v ∈ P a parameter, and a ∈ L A,P a parametrized action, B A,P is the set of boolean expressions (guards) overL A,P . Definition (pLTS) A parametrized LTS is a tuple P, S , s 0 , L, → where:

• P is a finite set of parameters, from which we construct the term algebra L A,P .

• S is a set of states; each state s ∈ S is associated to a finite indexed set of free variables f v(s) = x J s ⊆ P.

• s 0 ∈ S is the initial state.

• L is the set of labels, → the transition relation →⊂ S × L × L.

• Labels have the form l = α, e b , x J s := e J s such that if s → s, then:

1) α is a parametrized action, expressing a combination of inputs iv(α) ⊆ P (defining new variables) and outputs oe(α) (using action expressions).

2) e b ∈ B A,P is the optional guard.

3) The variables x J s are assigned during the transition by the optional expressions e J s with the constraints:

f v(oe(α)) ⊂ iv(α) ∪ x J s and f v(e b ) ∪ f v( e J s ) ⊆ iv(α) ∪ x J s ∪ x J s .
The networks of pLTSs (called pNets) are inspired by the synchronisation vectors of Arnold and Nivat [START_REF] Arnold | Finite Transition Systems: Semantics of Communicating Systems[END_REF], that is used to synchronise a (potentially infinite) number of processes. The holes in pNets can be indexed by a parameter, to represent (potentially unbounded) families of similar arguments. We represent the definition of pNets taken from [START_REF] Barros | Behavioural models for distributed Fractal components[END_REF] as below: Definition (pNets) A pNet is a tuple P, pA G , J, p J , O J , -→ V where: P is a set of parameters, pA G ⊂ L A,P is its set of (parametrized) external actions, J is a finite set of holes, each hole j being associated with (at most) a parameter p j ∈ P and with a sort O j ⊂ L A,P .

-

→ V = { - → v } is a set of synchro- nisation vectors of the form: - → v = α g , {α t } i∈I,t∈B i such that: I ⊆ J ∧ B i ⊆ Dom(p i ) ∧ α i ∈ O i ∧ f v(α i ) ⊂ P.
Each hole in the pNet has a parameter p j , expressing that this "parametrized hole" corresponds to as many actual pro-cesses as necessary in a given instantiation of its parameter. In other words, the parametrized holes express parametrized topologies of processes synchronised by a given Net. Each parametrized synchronisation vector in the pNet expresses a synchronisation between some instances ({t} t∈B i ) of some of the pNet holes (I ⊆ J). The hole parameters being part of the variables of the action algebra can be used in communications and synchronisations between the processes.

Timed specification

In this section, we present the preliminary denotations and definitions of timed-actions, logical clocks, clock relations and timed specifications. We shall use one example (Fig. 2) to illustrate all definitions and results. We choose a small scenario taken from the field of ITS. It is about an autonomous lane change involving three smart cars. These cars are equipped with sensors to detect the physical environment and parameters (e.g. such as cars' speeds, cars distances, etc.). And they communicate among each other to coordinate their movements and avoid collisions. Assume the three vehicles (car0, car1 and car2) are running on a road as Fig. 2.

Fig. 2 Car insertion

The scenario of inserting car0 between car1 and car2 may follow the following steps: 1) car0 gets a change-lane request (e.g. from a human user); 2) car0 sends "notify" requests to car1 and car2 to ask for an agreement; 3) car1 (resp. car2) acknowledges car0 "yes" or "no"; 4) car0 collects the results from car1 and car2; 5) if both car1 and car2 answer "yes", car0 signals the consensus to car1 and car2 and then goes to step 5, otherwise car0 aborts the procedure; 6) car1 slows down and/or car2 speeds up to leave more space between them for car0; 7) car0 changes its direction and moves to lane 2; 8) car0 notifies the end of the procedure with a "finish" signal.

As we do not want to limit ourselves to a specific language and a specific communication model, we follow the pNets assumption on action algebra L A,P which includes all required operators for building action expressions in the language (P is a set of parameters that are used to build open expressions, typically expressing data variables) [START_REF] Barros | Behavioural models for distributed Fractal components[END_REF]. In our model, we define L A,P,T as the timed-action algebra, in which T is a set of (discrete) timed variables. We denote for example α (∈ L A,P,T ) as an action name, then we consider α, !α(m) and ?α(m) as timed-actions. α means that the timed-action executes locally but not delivers messages. !α(m) (m ∈ P) is denoted as sending a message and ?α(m) (m ∈ P) as receiving a message. Definition 1 (timed-actions) Let T be a set of discrete time variables with domains in the non-negative natural numbers N. The timed-action algebra L A,T ,P is an action set built over T and P. We call α(p) t ∈ L A,T ,P a timed-action in which α ∈ A is an action, p ∈ P is a parameter, t ∈ T is a time variable describing a time delay before the action can be executed.

We set α 0 = α, which means the action α is always ready.

We define a Clock as a sequence of occurrences of a timedaction. The clock, in the sense of CCSL, is a logical clock, which is firstly proposed by Lamport [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF]. The logical clock means the distance between occurrences is not related with the passage of real time.

To preserve this independence with respect to any notion of global time, in the following definitions and proofs, we use only the notions of co-occurrence (α_i ≡ β_ j), and of precedence (α_i ≺ β_ j) of action occurrences. This will stay valid in any interpretation of the logical time scales. Definition 2 (clock) A Clock C α is a sequence of occurrences of a timed-action α(p) t . We write:

C α = {α(p 1 ) t α 1 _1, α(p 2 ) t α 2 _2, . . . , α(p i ) t α i _i, . . .} (i ∈ N), in which α(p i ) t α i _i denotes the i th occurrence of clock C α .
For simplification, in our paper, an occurrence α(p i ) t α i _i can be denoted as α_i for short when not ambiguous.

The assignment of the delay variable t α i in each occurrence α(p i ) t α i _i can be different. The delay variable captures the minimum time (delay) that an action must wait before it can occur after the previous action. More precisely when a clock is independent (has no precedence relation with another clock), the delay is counted from the previous occurrence of the same action as shown in the Fig. 3.

If a clock C β directly precedes a clock C α , then the delay of the ith occurrence of the timed-action α is counted from the ith occurrence of the timed-action β as shown in the Fig. 4. The relation of coincidence (discussed in the next subsec-tion) does not effect on the way of counting the delay. For example, if there is another clock C γ that coincides with the clock C α , then the delay t α i is still be counted as shown in the Fig. 4.

C Δ(n) α = {C α [n + 1]_1, C α [n + 2]_2, . . . , C α [n + i]_i, . . .}.
From the definition we can see that the (n + 1)th occurrence of C α becomes the first occurrence of the new clock C Δ(n) α , and so on.

Definition 4 (clock filtering) Assume N is a subset of N. Let C α be a clock built over a timed-action α. The new clock that is filtered from the clock C α by N is denoted as

C N α = {C α [i 1 ]_1, C α [i 2 ]_2, . . . C α [i k ]_ j, . . .}(i 1 , i 2 , . . . i k , . . . ∈ N , i 1 < i 2 < . . . < i k , . . . , j, k ∈ N).
For convenience, we will write the filter N either as a boolean function over N, or as a subset of N, e.g.: C {2n-1} n∈N α accepts only the odd occurrences of the clock C α . C {n 8} α filters out the first 8 occurrences.

More clearly, if

C α = {α(p 1 ) t α 1 _1, α(p 2 ) t α 2 _2, . . ., α(p i ) t α i _i, . . .}, then C {2n-1} n∈N α = {α(p 1 ) t α 1 _1, α(p 3 ) t α 3 _2, . . . α(p (2n-1) ) t α (2n-1) _n, . . .}. C {n 8} α = {α(p 8 ) t α 8 _1, α(p 9 ) t α 9 _2, . . .}
Finally in this section we define timed specifications. A timed specification is composed of a set of logical clocks, together with a set of clock relations, expressing the temporal ordering constraints between the clocks. This is an abstract specification in the sense that it captures just enough information to check the time safety (validity of time requirements) of a system, and the compatibility required for assembling subsystems together. In the following sections we shall describe procedures to compute the Timed Specifications of systems (timed-pLTSs and timed-pNets), and to check their compatibilities.

Definition 5 (timed specification) Let I C be the set of occurrences of the clock C. A rimed specification is a pair C, R where C is a set of clocks, R is a set of clock relations on C∈C I C .

Syntax and semantic of clock relations

A clock relation defines the relation between two clocks. With respect to the original definition of clock relations in CCSL [START_REF] André | Syntax and Semantics of the Clock Constraint Specification Language (CCSL)[END_REF], we have slightly different goals, and different needs. In particular we do not need exclusion (that is most important with some families of reactive formalisms). We do not define "subclock" relation in this paper because we need a more concrete way to define how to build a new subclock from original one. Instead, we defined "clock filtering" which can specify the way of selecting action occurrences. Therefore, here we only define two relation operations ('≺', '=') to describe the constraints between clocks.

Properties of the logical clock relations

Not surprisingly, these relations have their expected proper-ties: coincidence is an equivalence relation, and precedence is a strict pre-order.

α = C β ] = ∀i ∈ N, (α i ≡ β i ); (b) [C α ≺ C β ] = ∀i ∈ N, (α i ≺ β i )
C γ = C η ⇒ ∀i, γ_i ≡ η_i. If C α ≺ C γ ,
then according to the precedence definition, we know ∀i, α_i ≺ γ_i, which means the action α always occurs earlier than the action γ. Since ∀i, α_i ≡ β_i tells us the action α occurs if and only if the action β occurs, we know β always occurs earlier than γ (∀i, β_i ≺ γ_i). Similar, since ∀i, γ_i ≡ η_i tells us the action γ occurs if and only if the action η occurs, we furthermore have the relation ∀i, β_i ≺ η_i. According to the definition of precedence relations, we get

C β ≺ C η .
Example 1 In this part, we illustrate how to represent timed-actions, clocks, and clock relations for our "car inserting" scenario.

As shown in the Fig. 6, on-board car systems are modeled by several components including "Initial", "CommIni" "CommRes", "Control", etc. In the figure we only show the components that participate in the protocol.

User's requests are received by the "Initial" component. For example, the "user" has sent an insertion order, encoded here as a "!Request(Ins) t q " timed-action occurrence. The procedure then runs in two phases:

1) The agreement phase: car0 sends a noti f y(Ins) message to the other two cars, and waits for their answers. This phase is managed by the "CommIni" process, that communicates to the "ComRes" processes of other cars through asynchronous channels. In the model, there is one such channel for each type of messages, and for each pair of communicating processes; we use the parametrized structure of timed-pNets to represent such families of processes in the figure, e.g. "channelNtf[m]". The "CommIni" process is in charge of collecting the answers from the other cars asynchronously, and sending a final decision to "Initial" component. If it is negative, then "Initial" aborts and signals Cancel to the user, otherwise the procedure goes to the next phase.

2) The execution phase: this phase is triggered and controlled directly by the "Initial" process. It sends C !Consensus(ExpRes) to to all cars including itself to initiate the execution and to tell each car the final expected result ("Ex-pRes"). The "Control" process of each car is in charge of the local execution of the movement (that we leave unspecified here), till the expected result is observed ([ExpRes = CurData]). Then the !Finish signals are collected by "Initial", and a termination signal is notified to the user.

We use label transition systems (LTSs) to model each component. Each transition will be triggered by a clock. Precedence relations are used to specify the causality relations of LTSs. For example, in the "CommRes" component, the clock "C ?noti f y(Ins) tn " occurs earlier than the clock "C !ack(r m ) ta ". We denote the clock relation as "C ?noti f y(Ins) tn ≺ C !ack(r m ) ta ". For simplification, in the following sections, we will omit the parameters and time variables when expressing a clock relation if it is not ambiguous. For example, we use the short version "C ?noti f y ≺ C !ack " instead of "C ?noti f y(Ins) tn ≺ C !ack(r m ) ta ".

In this use-case, we assume for simplicity that the communication inside a car is synchronous (in realistic modern car systems, this hypothesis would have to be refined, since the onboard systems include several processes communicating through data buses). Here, the timed-action "!Cmd(par) t c " in the "Initial" process and the timed-action "?Cmd(par) t c " in "CommIni" are always synchronous when the two components communicate and transmit the message "par". So these two clocks coincide (C Initial.!Cmd(par) tc = C CommIni.?Cmd(par) tc ).

By contrast, communications between two different cars are asynchronous (typically over some wireless ad-hoc network). Since we want to be able to take into account the communication time in our analysis, we insert a specific asynchronous channel (built as a special timed-pLTS) for each type of messages exchanged between cars.

These two mechanisms illustrate our approach of modelling heterogeneous synchronous/asynchronous systems. In the next section, we show how we formalise this by using our timed-pNets formalism.

Timed-pLTS semantic model

This section introduces timed transition systems (timed-pLTS), including their special case channels. We illustrate each definition with a piece of our running example. Definition 6 (timed-pLTS) A timed-pLTS is a tuple P, S , s 0 , A, C, → , where

• P is a finite set of parameters.

• S is a set of states.

• s 0 ∈ S is the initial state.

• A is a set of timed-actions.

• C is a set of clocks over the timed-action set A.

• → is the set of transitions: →⊆ S × C × S . We write

s C α --→ s for (s, C α , s ) ∈→, in which α ∈ A.
Example 2 Consider the "CommIni" component in Fig. 7. The clock relations will correspond to the precedence (causality) relations between the transitions of the LTS, with a special case for the loops on states s 1 (a state for sending notifications) and s 2 (a state for receiving "ack" signals), where the communication events are indexed by k ∈ [1, 2, . . . , N] (N is the (fixed) number of neighbors of the initiating car (here N = 2)). The first loop on s 1 means that car0 sends a notification signal to car1 and car2, separately. The second loop on s 2 means that car0 collects "ack" signals from car1 and car2. Moreover, we use the silent action τ to build a clock C t τ τ that labels the transition to state s 2 when the component finishes sending two notifications. We build the timed-pLTS elements as:

• Parameters P = {k, Ins, r m , b, N}. • Action algebra A = {?Cmd(par) t c , !noti f y(par) t n , ?ack(k, r m ) t a , !R(b) t R , τ t τ }. • Clocks C = {C ?Cmd , C !noti f y , C ?ack , C !R , C τ }.
• We do not detail the clock relations here, they can be easily deduced from the figure.

Fig. 7 The timed-pLTS of the CommIni component Note that the system designers only need specify the timed-pLTSs. The clock relations can be automatically deduced from the timed-pLTSs (see Section 6).

Channels

We introduce channels to model asynchronous communication behaviours. A channel is defined as a special transition system with two timed-events: one for receiving messages, another for sending messages. A precedence relation is applied on the two events to model a delay of message transmissions. For simplification, the definition of channels here just describes a simple one place asynchronous buffer, sufficient to illustrate the heterogeneity of synchronous and asynchronous communications. More realistic asynchronous mechanisms are possible (e.g. n-places buffers, lousy channels, or ProActive/GCM request queues with futures [START_REF] Caromel | Asynchronous sequential processes[END_REF] but they are not the topics of this paper.

Definition 7 (channel)

A channel is a transition system with tuple P, S , A, C, ≺, → in which

• P is a finite set of parameters.

• S is the state set in which S = {s empty , s data }.

• A = {?in(par) t i , !out(par) t o } (par ∈ P) is the timedaction set.

• C is the set of clocks over timed-actions A.

• → is the set of transitions: s empty C ?in ---→ s data and

s data C !out ---→ s empty .
In the channel definition, the timed-action ?in(par) t i is an action for receiving messages from one component, while the timed-action !out(par) t o is an action for sending the messages to another component as shown in Fig. 8.

Fig. 8 The timed-pLTS of channel component

Timed-pNets semantic model

Here we define timed-pNets that are the nets of timed-pLTSs. Similar to the (untimed) pNets, a timed-pNet is a generalized composition operator, defining the synchronizations between a number of subsystems (holes). In timed-pNets, holes are characterized by timed-specifications. Building timed-pNets to represent a full system requires filling holes with (compatible) sub-nets.

Definition 8 (timed-pNets)

A timed-pNet is a tuple

P, A G , C G , J, A J , C J , R J , - → V
, where:

• P is a finite set of parameters.

• A G is a set of global timed-actions, and C G is the set of global clocks that are built over A G .

• J is a countable set of argument indexes: each index j ∈ J is called a hole and is associated with a set of local timed-actions A j , and an associated Timed Speci-

fication C j , R | . • - → V = { - → v } is a set of synchronization vectors of the form:
1) (binary communication between holes j 1 and j 2 )

- → v 1) = . . . , C !α , . . . , C ?α , . . . → C g , in which {C !α = C ?α = C g }, C g ∈ C G , C !α ∈ C j 1 , C ?α ∈ C j 2 , j 1 , j 2 ∈ J; 2) or (visibility from hole j) - → v = . . . , C α , . . . → C g , in which {C α = C g }, C g ∈ C G , C ?α ∈ C j , j ∈ J.
Furthermore, each global clock can be generated by only one synchronization vector:

∀ - → v i , - → v i ∈ - → V , C gi = C gi =⇒ - → v i = - → v i (C gi (resp. C gi ) be a global clock generated by the vector - → v i (resp. - → v i ), i, i ∈ N)
Remark We define timed-pNets in a form inspired by the 1) where ". . ." represents an arbitrary number of holes that do not participate in this synchronization synchronisation vectors of Arnold and Nivat [START_REF] Arnold | Finite Transition Systems: Semantics of Communicating Systems[END_REF], that we use to synchronise clocks from different processes. One of the main advantages of using its high abstraction level is that almost all interaction mechanisms encountered so far in the process algebra literature become particular cases of a very general concept: synchronisation vectors. We structure the synchronisation vectors as parts of network. Contrary to synchronisation constraints, the network allows dynamic reconfigurations between different sets of synchronisation vectors. In our timed-pNets, we define two kinds of synchronous vectors. One is the communication vector ( . . . , C !α , . . . , C ?α , . . . → C g ). The vector represents the communication of two holes through clock C !α and C ?α . The two local clocks that come from different holes are put between the two symbols " " and " ". The last element of the vector appears behind the symbol "→", and specifies the global clock generated by this synchronous vector. Another vector ( . . . , C α , . . . → C g ) makes the local clock C α visible by generating a global clock C g . For both kinds of synchronous vectors, the local clocks (that appear between " " and " ") are transparent to the upper layer nodes. Only the global clocks (the last elements in the synchronous vectors) can be observed from the upper level. These global clocks can be used for building a higher level timed-pNets node. Moreover, from the Definition 8 we can see that the synchronous vectors only catch the coincidence relations between clocks (for describing synchronous communications), which makes our timed-pNets models cannot directly specify asynchronous communications. So when modelling asynchronous communications, we need introduce channels into systems. The two subsystems that asynchronously communicate with each other are connected by a channel in which a communication delay is modelled. Example 3 shows us how to take advantage of channels to specify asynchronous communications.

Notations for parameterized systems. In practice, we use parametric notations, both for holes and for synchronization vectors, making the notations more compact and more userfriendly (see next example). These are only abbreviations, their meaning must be understood as a (finite) expansion of the structure.

Using such abbreviations, for a timed-pNet in which j 1 , j 2 , j are parametric holes with indexes k 1 , k 2 , k, with respective domains Dom 1 , Dom 2 , Dom, the synchronization vectors will look like: 1) Binary communication. Depending on the combina-tion of actions from j 1 and j 2 , this vector will generate a family of global actions indexed by a parameter m, that is a function of k 1 and k 2 . The domain of m is a subset of the product

Dom 1 × Dom 2 . . . . , C !α[k 1 ] , . . . , C ?α[k 2 ] , . . . → C g[m] , in which {C !α[k 1 ] = C ?α[k 2 ] = C g[m] }, C g[m] ∈ C G , C !α[k 1 ] ∈ C j 1 , C ?α[k 2 ] ∈ C j 2
2) Visibility. Each visible action from hole j generates a corresponding global action. . . . ,

C α[k] , . . . → C g[k] , in which {C α[k] = C g[k] }, C α[k] ∈ C j , C g[k] ∈ C G .
Example 3 We take our use case to illustrate how to build a timed-pNets model. To make the example smaller, we have extracted here the respective "communication" subnets of those cars, and the channels by which they communicate.

Hereafter, we show how to build the timed-pNets of this small subsystem.

As shown in the Fig. 9, the subsystem consists of components "CommIni", "CommRes[m]", "ChannelNtf[m]" and "ChannelAck [m]". The components "ChannelNtf[m]" and "ChannelAck[m]" are channels in which the parameter "[m]" denotes to which car the corresponding channel transmits data. By using the parameter "m", we give a more compact representation of the model. According to our scenario, car0 sends a notification to car1 (resp. car2) via "Chan-nelNtf [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF]" (resp."ChannelNtf[2]"), and then car1 (resp.car2) answers an "ack" to car0 via "ChannelAck [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF]" (resp. Chan-nelAck[2]"). So in the upper layer timed-pNets node, we can link these components by building synchronous vectors. For example:

1) The vector 2) -, C !ack [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] , -, C c.?ack [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] → C ack g3 [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] represents the communications between the components "Comm-Res [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF]" and "ChannelAck [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF]" and generates the global clock "C ack g3 [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] ". Notice that even though we actually have 7 subnets (CommIni, CommRes [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF], CommRes [START_REF] Fidge | Logical time in distributed computing systems[END_REF], ChannelNtf [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF], ChannelNtf [START_REF] Fidge | Logical time in distributed computing systems[END_REF], ChannelAck [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF], ChannelAck [START_REF] Fidge | Logical time in distributed computing systems[END_REF]), using parameters we represent our pNet and its synchronous vectors with only 4 holes.

2) the vector C {2s-1} s∈N !noti f y , -, C c.?noti f y [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] , -→ C noti f y g1 [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] represents the communications between the components "CommIni" and "ChannelNt f [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF]" and builds a global clock "C noti f y g1 [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] " (remember C {2s-1} s∈N !noti f y is the clock built from the clock C !noti f y by choosing the occurrences with the odd indexes).

Following the timed-pNets definition, we can formalize this timed-pNets with details as: Fig. 9 A Timed-pNets with one of its implementations

• P = {k, Ins, m, r m , b}. • A G = {noti f y(Ins, k) t g1 g1 [m] , noti f y(Ins, k) t g2 g2 [m] , ack(r m , k) t g3 g3 [m] , ack(r m , k) t g4 g4 [m] , ?Cmd(Ins) t g5 g5 , !R(b) (t g6 g6 }. • C G = {C noti f y g1 [m] , C noti f y g2 [m] , C ack g3 [m] , C ack g4 [m] , C ?Cmd g5 , C !R g6 }. • J = {CommIni, CommRes[m], ChannelNt f [m], ChannelAck[m]}(m := 1, 2).
Next we formalize the Timed Specifications of these holes as:

• For the hole "CommIni":

A CommIni = {?Cmd(Ins) t c , !noti f y(Ins, k) t n , ?ack(k, r m ) t a , !R(b) t R } C CommIni = {C ?Cmd , C !noti f y , C ?ack , C !R } R CommIni = {C ?Cmd ≺ C {2s-1} s∈N !noti f y , C {2s-1} s∈N !noti f y ≺ C {2s} s∈N !noti f y , C {2s-1} s∈N !noti f y ≺ C {2s-1} s∈N ?ack , C {2s} s∈N !noti f y ≺ C {2s} s∈N ?ack , C {2s-1} s∈N ?ack ≺ C {2s} s∈N ?ack , C {2s} s∈N ?ack ≺ C !R ≺ C Δ(1) ?cmd } • For the hole "CommRes[m]" (m := 1, 2): A CommRes[m] = {?noti f y(Ins, k) t n [m] , !ack(k, r m ) t a [m] } C CommRes[m] = {C ?noti f y [m] , C !ack [m] } R CommRes[m] = {C ?noti f y [m] ≺ C !ack [m] ≺ C Δ(1) ?noti f y [m] } • For the hole "ChannelNtf[m]" (m := 1, 2): A ChannelNt f [m] = {c.?noti f y(Ins, k) t n1 [m] , c.!noti f y(Ins, k) t n2 [m] } C ChannelNt f [m] = {C c.?noti f y [m] , C c.!noti f y [m] } R channelNt f [m] = {C c.?noti f y [m] ≺ C c.!noti f y [m] ≺ C c.?noti f y Δ(1) [m] } • For the hole "ChannelAck[m]" (m := 1, 2): A ChannelAck[m] = {c.?ack(k, r m ) t a1 [m] , c.!ack(k, r m ) t a1 [m] } C ChannelAck[m] = {C c.?ack [m] , C c.!ack [m] } R channelAck[m] = {C c.?ack [m] ≺ C c.!ack [m] ≺ C Δ(1) c.?ack [m] }
In the end, we specify the synchronous vectors: [START_REF] Fidge | Logical time in distributed computing systems[END_REF] , -, C c.?ack [START_REF] Fidge | Logical time in distributed computing systems[END_REF] → C ack g3 [START_REF] Fidge | Logical time in distributed computing systems[END_REF] ,

- → V = { V 1 : C {2s-1} s∈N !noti f y(Ins,k=1) , -, C c.?noti f y(Ins) [1] , -→ C noti f y g1 [1] , V 2 : -, C ?noti f y [1] , C c.!noti f y [1] , -→ C noti f y g2 [1] , V 3 : -, C !ack [1] , -, C c.?ack [1] → C ack g3 [1] , V 4 : C {2s-1} s∈N ?ack(k=1,r m ) , -, -, C c.!ack(r m ) [1] → C ack g4 [1] V 5 : C {2s} s∈N !noti f y(Ins,k=2) , -, C c.?noti f y(Ins) [2] , -→ C noti f y g1 [2] , V 6 : -, C ?noti f y [2] , C c.!noti f y [2] , -→ C noti f y g2 [2] , V 7 : -, C !ack
V 8 : C {2s} s∈N ?ack(k=2,r m ) , -, -, C c.!ack(r m ) [2] → C ack g4 [2] V 9 : C ?Cmd , -, -, -→ C ?Cmd g5 , V 10 : C !R , -, -, -→ C !R g6 }
Discussion Timed specification of holes. Let us now argue how the timed specifications of the holes in the upper-level timed-pNet node may have been specified, in a top-down approach, before building their timed-pLTS implementations. This, intuitively, is done from the informal description of the scenario and the architecture knowledge of the top level components and communications: Take the "CommIni" component as an example, the scenario related to the component is:

1) the component "CommIni" gets a change-lane request by clock C ?cmd from the "Initial" component;

2) the component "CommIni" sends requests by clock C !noti f y , in sequence, to car1 and car2 to ask for agreements;

3) the component "CommIni" collects results from car1 and car2 by clock C ?ack ;

4) the component reports a result to "Initial" component by clock C !R .

Since step 1) happens earlier than the step 2), the clock C ?cmd must precede the clock C !noti f y . Then, in our use case, the component "CommIni" sends a notification signal twice, so we have clock relation

{C ?Cmd ≺ C {2s-1} s∈N !noti f y ≺ C {2s} s∈N !noti f y }.
In generally, if there are N neighbors, the clock relation should be

{C ?Cmd ≺ C {Ns-(n-1)} s∈N !noti f y ≺ C {Ns-(n-2)} s∈N !noti f y ≺ . . . ≺ C {Ns} s∈N
!noti f y }. Similar to the step 2), since the component receives the "ack" signal twice, so we have the clock relation {C {2s

≺ C !R }.
Since the scenario is repeatable, we specify the clock relation

{C !R ≺ C Δ(1)
?cmd }. In the end, we conclude:

R CommIni = {C ?Cmd ≺ C {2s-1} s∈N !noti f y , C {2s-1} s∈N !noti f y ≺ C {2s} s∈N !noti f y , C {2s-1} s∈N !noti f y ≺ C {2s-1} s∈N ?ack , C {2s} s∈N !noti f y ≺ C {2s} s∈N ?ack , C {2s-1} s∈N ?ack ≺ C {2s} s∈N ?ack , C {2s} s∈N ?ack ≺ C !R ≺ C Δ(1)
?cmd } In Section 6, we will show that the timed specifications of the holes in Fig. 9 are indeed fulfilled by the corresponding timed-pLTS of "CommIni", "ComRes", "ChannelNtf", and "ChannelAck".

Compatibility

When assembling timed-pNets, the architect has to ensure that the timed-pLTSs that will be plugged into holes indeed match the timed specifications of these holes. The ultimate goal is to provide a refinement-based approach: the time properties proved on an open (abstract) timed-pNet system will be preserved by the refinements of Timed Specifications. One of the basic approaches for building such refinements is to ensure the compatibility of a subsystem with the enclosing holes before composing the system. For example, in Fig. 10, the timed specification (TS) of the subsystem "A_Impl" must be compatible with T S A , and each of the "C_Impl" must be compatible (individually) with T S C .

Our notion of compatibility is based on the inclusion relations between the clock relation sets. Before giving its formal definition, we introduce the concepts of "saturated relation set" and "relation set inclusion".

+ = {C 1 ≺ C 2 ≺ C 3 , C 1 ≺ C 3 , C 1 = C 1 , C 2 = C 2 , . . .} Definition 10 (inclusion of time specifications) Given two timed specifications T S 1 = C 1 , R 1 and T S 2 = C 2 , R 2 . Let R + 1 (resp. R + 2 )
be the saturated relation of T S 1 (resp. T S 2 ). We say T S 2 includes T S 1 (denoted as

T S 1 T S 2 ) if and only if C 1 ⊆ C 2 ∧ R 1 ⊆ R + 2 .
According to the definition, T S 1 T S 2 means that the relation existing in the timed specification T S 1 must exist in Fig. 10 Partial instantiation of a timed-pNets subsystem T S 2 or can be deduced from the relations in T S 2 . For example, assume

T S 1 = {C 1 ≺ C 3 }, T S 2 = {C 1 ≺ C 2 ≺ C 3 }.
According to the transitivity property of the "≺", we can get the the saturated relation set of the T S 2 as

R + 2 = {C 1 ≺ C 2 ≺ C 3 , C 1 ≺ C 3 , C 1 = C 1 , C 2 = C 2 , . . .}.
Since the relation in T S 1 can be deduced from the relations in T S 2 , we say T S 2 includes T S 1 (T S 1 T S 2 ).

Lemma 1 If T S 1 = C 1 , R 1 and T S 2 = C 2 , R 2 are two timed specifications, then T S 1 T S 2 =⇒ R + 1 ⊆ R + 2 Proof Taken any two relation r 1 , r 1 ∈ R 1 . Let r + 1 ∈ R +
1 be the relation deduced from the two relations r 1 , r 1 in terms of the property P proposed in Section 3. Assume r

+ 1 R + 2 . Since T S 1
T S 2 , from the definition of inclusion we know

R 1 ⊆ R + 2 . Furthermore, we know r 1 , r 1 ∈ R + 2 . So in the set R + 2
we can get the relation r + 1 by using the same property P. So we have r + 1 ∈ R + 2 that is in contradict with our assumption. Therefore, we have r

+ 1 ∈ R + 2 . Moreover, because r + 1 ∈ R + 1 , we can get R + 1 ⊆ R + 2 .
Definition 11 (compatibility) Let T S be the timed specification of a timed-pNets hole H, and T S be the timed specification of an implementation H_Impl. We say H_Impl is compatible with H, denoted by H_Impl H if and only if T S T S .

Theorem 1 Let T S be the timed specification of hole H. Let T S 1 (resp. T S 2 ) be the timed specification of an implementation H_Impl 1 (resp. H_Impl 2 ). If H_Impl 1 H and T S 1 T S 2 , then H_Impl 2 H.

Proof Assume T S 1 = C 1 , R 1 , T S 2 = C 2 , R 2 and T S = C, R . Let R + 1 (resp. R + 2 , R +
) be the saturated relation from T S 1 (resp. T S 2 , T S ). Since H_Impl 1 H, according to the refinement relation, we have T S T S 1 . Furthermore, according to the Inclusion definition, we have R ⊆ R + 1 . Moreover, because we know that T S 1 T S 2 , according to the Lemma 1, we have

R + 1 ⊆ R + 2 .
According to the set theory, we know that R ⊆ R + 2 . Finally, according to the Inclusion and refinement relation definition, we get H_Impl 2 H.

Generating the timed specification of a timed-pLTS

As we see in the Fig. 9, timed-pLTSs are concrete implementations of those holes. In order to check the compatibility, we need to generate timed specifications for those concrete timed-pLTSs. Here we propose rules to automatically gener-ate the timed specifications from the timed-pLTSs. More precisely, given the action algebras and the transition relations of a timed-pLTS, we can get a set of clocks, and the relations between these clocks. This procedure runs in 4 phases as shown in the Fig. 11. The inputs of the procedure include a timed-pLTS and a set of rules that tell how to set the occurrence relations and its index functions. In Step 1, we traverse the timed-pLTS and generate a "symbolic" table that gathers all possible causally related pairs of transitions of the timed-pLTS, and the corresponding relations between clock occurrences. In Step 2 we go through the symbolic table and build a "concrete" table in which each column represents one specific "round" of execution through the symbolic table (with concrete index assignments). In the concrete table guards of the timed-pLTS can be resolved, so some of the symbolic transitions may be eliminated. In Step 3 we generate a general formula for each relation. In the end (Step 4), we lift those occurrence relations to clock relations, and generate the timed specification. For a timed-pLTS transition system P, S , s 0 , A, C, → , we denote PreAct(s, s ) as the set of direct preceding timed-action occurrences of s from s , and PostAct(s, s ) as the set of direct succeeding timed-action occurrences of state s towards state s . Then we denote PreAct(s) (resp. PostAct(s)) as the set of all direct preceding (resp. succeeding) timedaction occurrences of state s. Furthermore, we define PreActIndex(s) (resp. PostActIndex(s)) as the sum of the indexes of the set of preceding (resp. succeeding) timed-action occurrences of state s. The sum corresponds to the cases where branches in the LTS allow some executions to go several times through alternative transitions out of some states.

Definition 12 (preceding timed-action occurrences) Let

P, S , s 0 , A, C, → be a timed-pLTS transition system. For s ∈ S and α(p) t α ∈ A, (p ∈ P), the direct preceding timed-action occurrence of s is defined as PreAct(s, s ) = {α_i|s

C α --→ s, α_i ∈ C α , } (s, s ∈ S ).
The set of direct preceding timed-action occurrences of s is defined as PreAct(s) = s ∈S PreAct(s, s ). Furthermore, we denote the index of a preceding timed-action occurrence as PreActIndex(s, s

) = {i|s C α --→ s, α_i ∈ C α (s, s ∈ S )},
and the sum of the indexes of a set of preceding timed-action occurrences of state s as PreActIndex(s) = s ∈S PreActIndex(s, s ).

Definition 13 (succeeding rimed-action occurrences] Let

P, S , s 0 , A, C, → be a timed-pLTS transition system. For s ∈ S and α(p) t α ∈ A, (p ∈ P), the direct succeeding timedaction occurrence of state s is defined as PostAct(s, s ) = {α_i|s C α --→ s , α_i ∈ C α }, (s, s ∈ S ). The set of direct succeeding timed-action occurrences of state s is defined as PostAct(s) = s ∈S PostAct(s, s ). Furthermore, we denote the index of a succeeding timed-action occurrence as

PostActIndex(s, s ) = {i|s C α --→ s , α_i ∈ C α }, (s, s ∈ S )
, and the sum of the indexes of a set of succeeding timed-action occurrences of s as PostActIndex(s) = s ∈S PostActIndex(s, s ).

Relations and assignment rules

The computation in Step 1 is based on a set of rules that identify specific configurations of the states in the timed-pLTS traversal. For each such configuration, we have a rule that expresses the relation(s) between the set of preceding and succeeding clock occurrences of the current state, and the changes in the clock occurrence indexes.

The main configurations are: initial state, in which we have to initialize indexes, and increase an index each time the system goes through a new global round; standard state in which we register the increase of one of the involved index; and looping states, in which we have to take care of the guards for entering/leaving loops, in terms of a specific "loop counter".

We define a restrictive notion of looping state which is reasonable configuration for timed analysis. A looping state may have one or more loops of arbitrary length, but coming back to the same state. And each loop must start with a transition with a guard taking the precise form of a "loop counter" control, namely [k=1; k++; k kMax] for some counter variable k, in which kMax may be a positive natural number, or a variable. Loop guards can share a loop counter (see e.g. Fig. 12), so several loops will be executed the same number of times; otherwise different loop counters must be independent. Of course one could imagine more complex structures for our timed-pLTSs, but this restriction already covers a lot of interesting cases, and make the generation of the times specification easier.

In these rules, for simplification, we represent relations on two sets (S 1 (resp. S 2 ) is a set of occurrences of clocks):

S 1 ≺ S 2 means ∀α m ∈ S 1 , β n ∈ S 2 , α m ≺ β n (m, n ∈ N). 1) Initial state. If PreAct(s 0 ) ∅, then PreAct(s 0 ) ≺ PostAct(s 0 ), [ Assign: PostActIndex(s 0 ) ⇐ PreActIndex(s 0 ) + 1 ]; 2)
s 0 tr0 : s 2 C !R ---→ s 0 C ?Cmd -----→ s 1 !R_m ≺ ?Cmd_n f tr0 : n = m + 1 s 1 tr1 : s 0 C ?Cmd -----→ s 1 Cτ --→ s 2 ?Cmd_n ≺ τ_r f tr1 : r = n tr2 : s 0 C ?Cmd -----→ s 1 C !Noti f y ------→ s 1 ?Cmd_n ≺ !noti f y_i f tr2 : i := i + 1 tr3 : s 1 C !Noti f y ------→ s 1 C !Noti f y ------→ s 1 !noti f y_i ≺!noti f y_(i + 1) tr4 : s 1 C !Noti f y ------→ s 1 Cτ --→ s 2 !noti f y_i ≺ τ_r f tr4 : r = n s 2 tr5 : s 1 Cτ --→ s 2 C !R ---→ s 0 τ_r ≺!R_m f tr5 : m = r tr6 : s 1 Cτ --→ s 2 C ?Ack ----→ s 2 τ_r ≺ ?ack_ j f tr6 : j := j + 1 tr7 : s 2 C ?Ack ----→ s 2 C ?Ack ----→ s 2 ?Ack_ j ≺ ?ack_( j + 1) tr8 : s 2 C ?Ack ----→ s 2 C !R ---→ s 0 ?Ack_ j ≺!R_m f tr8 : m = r

The method for generating timed specification

This subsection introduces a method of generating timed specifications from timed-pLTSs. We state two algorithms and 4 steps.

Step 1: generate occurrence relations table

The Algorithm 1 uses the rules above to build an occurrence relation Example 4 Let us take the "CommIni" component from Fig. 7 as an example. We first transform Fig. 7 into Fig. 12 by removing all parameters but adding index variables. Then we generate occurrence relations for each state. For example, we take the state "s 0 ", from the timed-pLTS graph we get transitions s 2

C !R --→ s 0 C ?Cmd ----→ s 1 .
According to the rule 1) we have !R_m ≺?Cmd_n and the assignment n = m + 1 (n, m ∈ N). Take the state s 1 as another example. Since it includes a selfloop, we apply the rules 2), a), b) and II). When a transition directly brings to next state without passing the loop, according to the rule 2), we have the relation ?Cmd_n ≺ τ_r and the assignment r = n. When a transition enters the loop, according to the rule a), we have the relation ?Cmd_n ≺ !noti f y_i and the assignment i := i + 1 (i ∈ N). When a transition stays in the loop, according to the rule b), we can get the relation "!noti f y_i ≺ !noti f y_i + 1" (i ∈ N). Then when a transition leaves the loop, according to the rule II), we have the relation !noti f y_i ≺ τ_r and the assignment r = n (r ∈ N).

table built in

Step 1 and then generate a "concrete" table in which each column represents one specific "round" of execution through the symbolic table (with concrete index assignments). In the concrete table the guards of the timed-pLTS can be resolved, so some of the symbolic transitions (rows of the table) may be eliminated.

In the guards (including the loop control guards), there may be some parameters occurring in a symbolic form. Before we run the algorithm in Step 2, we need to instantiate these parameters, to be able to compute the guards. In particular the maximum value of the loop counters (in our use-case, corresponding to the number of neighbor cars) must be fixed.

Moreover, we must set a bound (N) to the number of rounds that we shall unfold in the algorithm. This bound should be large enough for the generalization procedure in Step 3 to work properly.

For each round of traveling, we compute a set of occurrence relations. The indexes of these occurrences tell the (logical) times of the actions that have occurred till this round. For the loops, the loop control guard says that if a transition satisfies the initial condition "k = 1", then the transition goes into the loop. Each time after executing the loop, the variable k increases by 1. Then the transition continues to execute the loop till the condition k kMax is not satisfied.

We present Algorithm 2 to enumerate these relations. The results of the algorithm are illustrated in the table in the Table 2 in which the rth column presents a set of occurrence relations in the round r, and the jth row presents a sequence of relations on two clock occurrences.

Example 5 Take the component "commIni" as an example, we enumerate its occurrence relations. Let all occurrence index variables initially be 0 (m, n, r, i, j := 0) and the loop control variable k be 1 (k := 1). Starting from s 0 , we get the transition tr0 : s 2

C !R --→ s 0 C ?Cmd ----→ s 1 .
From the first line of the Table . ??, we get n = 1 (because m = 0 and f tr0 : n = m + 1) and so we get the relation !R_0 ≺ ?Cmd_1. Then the transition goes to s 1 . Since k := 1, the transition goes into the self-loop. So we get the transition tr2 : s 0

C ?Cmd ----→ s 1 C !Noti f y -----→ s 1 .
From the third line of Table. ??, we can compute i = 1 (because f tr3 : i := i + 1) and then we get the relation ?Cmd_1 ≺!Noti f y_1. According to the loop control, we know k increases by 1 (k + +), so k = 2. Since the condition k 2 is still satisfied, the transition goes into the self-loop again. According to the transition tr3 : s 1

C !Noti f y -----→ s 1 C !Noti f y -----→ s 1 ,
if tr = s Cα --→ s C β --→ s then Indexo f (C β ) ← compute by f tr R[ j][r] = α_Indexo f (C α ) ≺ β_Indexo f (C β ) C ← C -C α -C β j + + s ← s; s ← s ; s ← one from PostAct(s) that satisfies a certain guard; C α := C β C β := {C β |s C β --→ s } end if end for end while reset C with n clocks C = {C 1 , C 2 , . . . C n } end while
!R_0 ≺ ?Cmd_1 !R_1 ≺ ?Cmd_2 !R_2 ≺ ?Cmd_3 !R_(s -1) ≺ ?Cmd_s . . . C !R ≺ C Δ(1) ?Cmd ?Cmd_1 ≺ !noti f y_1 ?Cmd_2 ≺ !noti f y_3 ?Cmd_3 ≺ !noti f y_5 ?Cmd_s ≺ !noti f y_(2s -1) . . . C ?Cmd ≺ C {2s-1} !noti f y !noti f y_1 ≺!noti f y_2 !noti f y_3 ≺!noti f y_4 !noti f y_5 ≺!noti f y_6 !noti f y_(2s -1) ≺!noti f y_2s . . . C {2s-1} !noti f y ≺ C {2s} !noti f y !noti f y_2 ≺ τ_1 !noti f y_4 ≺ τ_2 !noti f y_6 ≺ τ_3 !noti f y_2s ≺ τ_s . . . C {2s} !noti f y ≺ C τ τ_1 ≺ ?ack_1 τ_2
C !Noti f y -----→ s 1 C τ --→ s 2 .
According to the Table 1, we know r = 1 (because f tr4 : r = n). Then the state s 2 is similar as the state s 1 . In the end of this inner loop we get the first column of the Table 2. Remark that the rows corresponding to transitions tr1 and tr5 from the Table 1 have been eliminated in this process, because the corresponding loops cannot exit immediately. Then by repeating the second round, third round, etc, we can get the relations listed in the second column, the third column of the Table 2, etc., until we reach the column N.

Step 3: Generalize the occurrence relations

In the Table 2, in each line we get a sequence of occurrence relations. To induce the corresponding general relation, we transfer the problem to find a general formula for a sequence of nature numbers. We could use here standard arithmetic methods (e.g. Neville's algorithm [START_REF] Bulirsch | Introduction to Numerical Analysis[END_REF]) that are able to automatically deduce polynomial formulas for a given set of unrepeatable natural number sequences. However, such a general approach would make difficult to estimate the minimum number of unfolding required for finding the general formula. But in fact, due to our hypothesis on the independence of the loop control counters, the formula we seek here will be linear in the clock indexes, and the length of unfolding may be estimated from the maximum value of the loop indexes. A proof of this property, and a detailed estimation of the bound, is out of the scope of this paper. The result of generalisation is shown in "column s" in the Table 2.

Example 6 Let us go on the Fig. 12 as an example. Since the loop counter is two, so we need unfold the relations at most for three times. As shown in the second line of the Table 2, the sequence of occurrence indexes of the clocks C ?Cmd and C !Noti f y are {1, 2, 3} and {1, 3, 5}. According to the Neville's algorithm, we can get the general formulas for the clock C ?Cmd as a n = n, and for the clock C !Noti f y as a n = 2n -1. So in the second line, the relation of the s round (∀s < 0)is ?Cmd_s ≺!Noti f y_{2s -1}.

Step 4: lifting to clock relations

In the last step, we lift the concurrence relations to clock relations, using the clock operators "lift" and "filter" from Definitions 3 and 4. This step is straightforward, and the result is shown in the last column of the Table 2.

Generating the timed specification of a timed-pNet

A timed-pNets node actually consists of a set of holes (J) with timed specifications (T S j ), synchronous vectors (V i ), and global clocks (C G ) generated from the synchronous vectors. Therefore, generating the external timed specification for a timed-pNets node (called global timed specification T S g ) boils down to compute the global clock relations from the local timed specifications of its holes (T S j ) and the coincidence relations deduced from the synchronous vectors (V i ), using the properties on clock relations from Section 2.

Definition 14 (global clock relation set) Given a timed-pNet T -pNets

= P, A G , C G , J, A J , C J , R J , - → V The global time specification of T -pNets is the pair C G , R G ,
where R G is the global clock relation set deduced from: 1) all local clocks relations R j from its holes; 2) the (coincidence) relations deduced from all its synchronization vectors; 3) symmetry and transitivity of coincidence, transitivity of precedence.

During this logical saturation process, it may happen that contradictory relations are deduced, when two clocks would be proved both coincident and precedent, or precedent both ways. We call this clock conflicts.

Definition 15 (clock conflicts) Given a timed specification

C, R : 1) two clocks C α and C β in C are in conflict if either C α = C β ∧ (C α ≺ C β ∨ C β ≺ C α ) ∈ R or C α ≺ C β ∧ C β ≺ C α ∈ R
2) the global clock conflict set of a timed-pNet is the set of pairs of clocks in conflict in its global clock relation set.

Example 7

Let us take Fig. 9 as an example. From the user specification in Example 3 (page 10), we know the clock relations of these holes are:

• R CommIni = {C ?Cmd ≺ C {2s-1} s∈N !noti f y , C {2s-1} s∈N !noti f y ≺ C {2s} s∈N !noti f y , C {2s-1} s∈N !noti f y ≺ C {2s-1} s∈N ?ack , C {2s} s∈N !noti f y ≺ C {2s} s∈N ?ack , C {2s-1} s∈N ?ack ≺ C {2s} s∈N ?ack , C {2s} s∈N ?ack ≺ C !R ≺ C Δ(1) ?cmd } • R ChannelNt f [m] = {C c.?noti f y [m] ≺ C c.!noti f y [m] ≺ C c.?noti f y Δ(1) [m] }, • R ChannelAck[m] = {C c.?ack [m] ≺ C c.!ack [m] ≺ C Δ(1) c.?ack [m] }, • R CommRes[m] = {C ?noti f y [m] ≺ C !ack [m] ≺ C Δ(1) ?noti f y [m] }.
Besides, we derive the clock relations from the synchronous communications defined by synchronous vectors as:

• R V 1 = {C {2s-1} s∈N !noti f y = C c.?noti f y [1] = C noti f y g1 [1] }, • R V 2 = {C c.!noti f y [1] = C ?noti f y [1] = C noti f y g2 [1] }, • R V 3 = {C !ack [1] = C c.?ack [1] = C ack g3 [1] }, • R V 4 = {C c.!ack [1] = C {2s-1} ?ack = C ack g4 [1] }, • R V 5 = {C {2s} s∈N !noti f y = C c.?noti f y [2] = C noti f y g1 [2] }, • R V 6 = {C c.!noti f y [2] = C ?noti f y [2] = C noti f y g2 [2] }, • R V 7 = {C !ack [2] = C c.?ack [2] = C ack g3 [2] }, • R V 8 = {C c.!ack [2] = C {2s} ?ack = C ack g4 [2] }, • R V 9 = {C ?Cmd = C ?Cmd g5 }, • R V 10 = {C !R = C !R g6 }.
Take the relation between the global clocks C noti f y g1 [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] and C noti f y g2 [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] as an example. It is generated by the synchronous vectors V 1 and V 2 , as well as the relations of hole ChannelNt f [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] . We deduce the relations C noti f y g1 [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF]

= (R V 1 ) C c.?noti f y [1] ≺ (R ChannelNt f [1] ) C c.!noti f y [1] = (R V 2 ) C noti f y g2 [1] , and con- clude C noti f y g1 [1] ≺ C noti f y g2 [1] .
The formal definition above is not very practical. Actually by analysing on the interactions between the synchronization vectors, we can compute a set of global clock relations that is sufficient to generate the global clock relation set. The Theorem 2 defines the case analysis procedure, and states its correctness (all relations computed are correct). The next Theorem 3 will prove its completeness. In Theorem 2, one particular case may detect a local conflicts between two global actions, more precisely between two synchronization vectors representing communications between the two holes. In this case, we shall signal the conflicts, but produce no relations between these actions. Other types of conflicts could be created by configurations involving more than two holes. These cannot be detected at the level of this case-analysis procedure. A full conflict detection procedure is out of the scope of this paper.

Theorem 2 (global clock relation analysis) Given a timed-pNet T -pNets

= P, A G , C G , J, A J , C J , R J , - → V . Let H α , H β , H γ be three holes of T -pNets and C H α , C H β , C H γ ⊂ C J be the sets of clocks of holes H α , H β and H γ . Let the clocks C α 1 , C α 2 ∈ C H α , the clocks C β 1 , C β 2 ∈ C H β , the clock C γ 1 ∈ C H γ , with C H α C H β C H γ = ∅).
For each pair of global clocks C a g1 and C a g2 , we enumerate the pairs of synchronization vectors that are able to generate them, and match them with the following cases (note that both pairs (C a g1 , C a g2 ) and (C a g2 , C a g1 ) will be enumerated, so we do not consider symmetric condi-tions in the cases below). Each match may add a clock relation in the global clock relation set R: 13(a), then:

1) if C α 1 = C α 2 ∧ C β 1 = C β 2 then (C a g1 = C a g2 ) ∈ R; 2) if C α 1 ≺ C α 2 ∧ C β 1 ≺ C β 2 then (C a g1 ≺ C a g2 ) ∈ R; 3) if C α 1 = C α 2 ∧ C β 1 ≺ C β 2 or if C α 1 = C α 2 ∧ C β 2 ≺ C β 1 then a conflict
1) if C β 1 = C β 2 then (C a g1 = C a g2 ) ∈ R; 2) if C β 1 ≺ C β 2 then (C a g1 ≺ C a g2 ) ∈ R.
1) if C β 1 = C β 2 then (C a g1 = C a g2 ) ∈ R; 2) if C β 1 ≺ C β 2 then (C a g1 ≺ C a g2 ) ∈ R.
Case 4 If the global clock C a g1 and C a g2 are generated from the synchronous vectors . . . , C β 1 , . . . → C a g1 and . . . , C β 2 , . . . , . . . → C a g2 as shown in Fig. 13(d) then:

1) if C β 1 = C β 2 then (C a g1 = C a g2 ) ∈ R, 2) if C β 1 ≺ C β 2 then (C a g1 ≺ C a g2 ) ∈ R.
Otherwise In other cases, this pair of clocks are NOT directly related in R.

Proof For each of the cases, we prove that the deduced relation is indeed correct with respect to Definition 14.

Case 1 From the two synchronous vectors . . . ,

C α 1 , . . . , C β 1 , . . . → C a g1 , . . . , C α 2 , . . . , C β 2 , . . . → C a g2 , we know that C α 1 = C β 1 = C a g1 and C α 2 = C β 2 = C a g2 . 1) If C α 1 = C α 2 ∧ C β 1 = C β 2 ,
according to the transitivity property of "=", we get the relation C a g1 = C a g2 .

Fig. 13 The four cases of Theorem 2

2

) If C α 1 ≺ C α 2 ∧ C β 1 ≺ C β 2 , then we have C a g1 = C α 1 ≺ C α 2 = C a g2 .
C β 1 = C γ 1 = C a g1 and C α 1 = C β 2 = C a g2 . 1) If C β 1 = C β 2 ,
then according to the transitivity property of "=", we know that

C a g1 = C a g2 . 2) If C β 1 ≺ C β 2 , since C a g1 = C β 1 ≺ C β 2 = C a g2 , then we have the relation C a g1 ≺ C a g2 .

Case 3 and Case 4

The proofs are similar to Case2.

Example 8 Let us take again the Fig. 9 as an example to compute the clock relation between C noti f y g2 [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] and C ack g3 [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] . We know the two global clocks are generated by the vectors V 2 : . . . , C c.!noti f y [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] , . . . , C ?noti f y [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] , . . . → C noti f y g2 [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] and V 3 : . . . , C !ack [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] , . . . , C c.?ack [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] , . . . → C ack g3 [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] . We are in case 2), and we know from T S {CommRes [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] } that C ?noti f y [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] ≺ C !ack [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] . So we conclude C noti f y g2 [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] ≺ C ack g3 [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] .

Theorem 3 (completeness) There exist four and only four combinations of synchronous vectors, as listed in Theorem 2, for deducing a relation between a pair of global clocks.

Proof From the timed-pNets definition, we know that there are two ways to build a global clock: binary communication and visibility. So there are three combinations:

Assembling a multi-layer timed-pNets system

After generating a timed specification for a timed-pNets node, we can use the generated timed specification to prove that it would be compatible with the specification of a hole of a higher-level pNet. This way, a layered tree structure can be built as shown in the Fig. 14. In this structure, each layer is an abstraction of its lower layer. The clocks in the lower layer (at level N) are transparent to its abstract layer (at level N+1) in which only holes with its timed specification (T S j ), synchronous vectors (V i ) and global clocks (C G ) can be seen. As we have already mentioned, this construction can be done in a very flexible way either bottom-up or top-down. So the consequence of timed-pNets can be open (if it still contains some unfilled holes at the leaves), or closed if all holes are filled with timed-pNets or timed-pLTSs.

Example 9

We now have all elements required for check-ing the compatibility of our timed-pLTSs with the holes of the upper layer pNet. Let us look at "CommIni" as an example: 1) the relation set of the hole "CommIni" for open timed-pNets is

R CommIni = {C ?Cmd ≺ C {2s-1} s∈N !noti f y , C {2s-1} s∈N !noti f y ≺ C {2s} s∈N !noti f y , C {2s-1} s∈N !noti f y ≺ C {2s-1} s∈N ?ack , C {2s} s∈N !noti f y ≺ C {2s} s∈N ?ack , C {2s-1} s∈N ?ack ≺ C {2s} s∈N ?ack , C {2s} s∈N ?ack ≺ C !R ≺ C Δ(1)
?cmd }, 2) the relation set of the "CommIni" timed-pLTS component from the Table 2 is

R Commini = {C ?Cmd ≺ C {2s-1} s∈N !noti f y ≺ C {2s} s∈N !noti f y ≺ C {2s-1} s∈N ?ack ≺ C {2s} s∈N ?ack ≺ C τ ≺ C !R ≺ C Δ(1) ?cmd }.
Since we can easily get R {CommIni} ⊆ R Commini , according to Inclusion definition we have T S {CommIni} T S Commini . Therefore, from the compatibility definition, we know that the "CommIni" timed-pLTS is compatible with the hole "CommIni".

The validations that have been defined in our paper, namely the compatibility of hole composition, and the conflict detection between timed-pNets synchronization vectors, ensure some specific validity properties of the global time specification of the system, as defined by Definition 14. However, this does not mean that there cannot be more complex conflicts in the interactions between more than two holes of timed-pNets, or more specific timed properties that can be computed from refined implementations of some sub-nets. In the next section, we show how to use simulation with the TimeSquare tool to address such cases.

Simulation

In this section we explain how to use TimeSquare [START_REF] Deantoni | TimeSquare: Treat your models with logical time[END_REF] to detect complex conflicts of timed-pNets. Two inputs are required by TimeSquare (see the Fig. 15). One is an open timed-pNets system. Another is a set of refined implementations. If the closed timed-pNets composed by those refined implementations have no conflicts, we say the closed timed-pNets are safe. Otherwise, the TimeSquare reports violations, which means that conflicts exist in the closed timed-pNets. Before running simulations, the two inputs are translated into timed specifications that are acceptable format for TimeSquare. The way of generating timed specifications is described in Sections 7 and 8.

Simulation 1

• We take the system shown in the Fig. 9 as an example.

We first build an open timed-pNet node with the timed [START_REF] Fidge | Logical time in distributed computing systems[END_REF] ; C ack g4 [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] ≺ C ack g4 [START_REF] Fidge | Logical time in distributed computing systems[END_REF] }. Then we import the timed specifications of the refined implementa- can see that the abstract specification T S g is satisfied by the refined concrete system since we have T S g T S g .

S g = C g , R g with R g = {C ?Cmd g5 ≺ C noti f y g1 [m] ≺ C noti f y g2 [m] ≺ C ack g3 [m] ≺ C ack g4 [m] ≺ C !R g6 ; C noti f y g1 [1] ≺ C noti f y g1

Simulation 2

• In this simulation, we choose T S {U pdatedCommIni} =

{C ?Cmd ≺ C {2s-1} !Noti f y ≺ C {2s-1} ?Ack ≺ C {2s} !Noti f y ≺ C {2s} ?Ack ≺ C !R ≺ C Δ(1) ?Cmd }, T S {U pdatedCommRes[m]} = {C ?Noti f yIn f o [m] ≺ C ExchangeIn f o [m] ≺ C !Ack [m]
} and we add a synchronous vector between hole CommRes [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] and CommRes [START_REF] Fidge | Logical time in distributed computing systems[END_REF]

to get a new relation R V new = {C ExchangeIn f o [1] = C ExchangeIn f o [2] = C ExchangeIn f o g11 }.
{C Noti f y g1 [2] ≺ C Noti f y g2 [2] ≺ C ExchangeIn f o g7 ≺ C Ack g3 [1] ≺ C Ack g4 [1] }. Obviously, relation {C Noti f y g1 [2] ≺ C Ack g4 [1]
} is hold in terms of the transitivity property of precedence relations. However, by using the theo-rem 2 again, from the T S {U pdatedCommIni} we can get the relation {C Ack g4 [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] ≺ C Noti f y g1 [START_REF] Fidge | Logical time in distributed computing systems[END_REF] } which is in contradict with the relation {C Noti f y g1 [START_REF] Fidge | Logical time in distributed computing systems[END_REF] ≺ C Ack g4 [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] }. To fix the conflict, we need to find another implementation that is still compatible with these holes without making conflicts. For our example, we can just simply change the T S {U pdatedCommIni} to T S {FixedCommIni} = {C ?Cmd ≺

C {2s-1} !Noti f y ≺ C {2s} !Noti f y ≺ C {2s-1} ?Ack ≺ C {2s} ?Ack ≺ C !R ≺ C Δ(1)
?Cmd }. And in the end, by simulation, no conflict exists any more. Globally asynchronous locally synchronous (GALS) [START_REF] Chapiro | Globally-asynchronous locally-synchronous systems[END_REF] is a model of computation that allows to design computer systems consisting of several synchronous components interacting with each other with asynchronous communication, e.g., FIFOs. It can be used both in software and hardware. In software, these synchronous components usually are specified as finite state machines (FSMs) and the asynchronous communication between them is modeled with a buffer [START_REF] Chiodo | Hardware-software codesign of embedded systems[END_REF]. The idea of the GALS approach provides a methodology for combining concurrent embedded systems within loosely coupled systems. Similar to the idea of GALS, Serrano designed the HipHop language [START_REF] Berry | Hiphop: a synchronous reactive extension for hop[END_REF] that follows the synchronous reactive model of the Multiclock Esterel [START_REF] Berry | Multiclock esterel[END_REF] to specify reactive program by dealing with abstract events and their reactions.

Our model partly takes this idea to specify both synchronous and asynchronous communication. The main difference is that we specify the synchronous components as timed specifications (a set of clocks and clock relations) instead of FSMs. Moreover, the synchronous communications are specified by the coincidence relations between clocks that come from different timed specifications, while the asynchronous communications are modeled by channels in which precedence relations are applied on two clocks. Timed-automata [START_REF] Alur | A theory of timed automata[END_REF] is famous for modeling the behaviour of real-time systems. They provided a simple and powerful way to annotate state transition graphs with time constraints using finitely real-value clocks. Closure properties, decision problems as well as automatic verification of real-time requirements were considered in timed-automata and supported by several tools like UPPAAL [START_REF] Bengtsson | Uppaal -a tool suite for automatic verification of real-time systems[END_REF]. Timed-automata can be a good reference for building and verifying timed models. However, the clocks in timed-automata are a finite set of realvalued clocks whose values increase all with the same speed. This feature does not help us to model systems consisting of independent-clock devices, since these clocks from different devices may have different speed.

BIP [START_REF] Basu | Modeling heterogeneous real-time components in BIP[END_REF] is a framework for the incremental composition of heterogeneous components. It allows building complex systems by coordinating the behaviour of a set of atomic components. The methodology based on the theory that components are obtained as the superposition of three layers. The lowest layer are the component behaviours that are described as automata extended with data and functions. The intermediate layer includes a set of connectors describing the interactions between transitions of the behaviours. The upper layer is a set of priority rules describing scheduling policies for interactions. BIP encompasses heterogeneity. It provides a powerful mechanism for structuring interactions involving strong synchronization (rendezvous) or weak synchronization (broadcast). Synchronous execution is characterized as a combination of properties of the three layers. However, modeling timed components in BIP involves references to a specific "tick" port expressing the passage of (discrete) time, and such "tick" events must be synchronized between various components of a system, before computing worst case execution time (WCET) or task period properties. With contrast to this approach, we do not want to assume the existence of a single reference clock, but rather let the various clocks as unrelated as possible.

Modeling and analysis of real-time and embedded system (MARTE) [START_REF] Graf | Modeling and analysis of real-time and embedded system[END_REF] is a special extension of UML for modeling real-time embedded systems. It defines the standard modelbased description for real-time and embedded systems and provides facilities to annotate models with information required to perform specific analysis. It supports modeling and analysis of component-based architectures, as well as a variety of different computational paradigms (asynchronous, synchronous, and timed). Recently, the idea of logical time and clock constraint specification language (CCSL) has been introduced into MARTE for its extension of modeling distributed systems. So it can be used to check the communication and causality path correctness by introducing event relations into models. However MARTE UML is large and com-plex. It comprises many different concepts and semantics that we do not need. Since we would like to keep the semantic as simple as possible, we choose pNet instead of MARTE to imply our idea.

Programming temporally integrated distributed embedded systems (PTIDES) [START_REF] Eidson | Distributed real-time software for cyber-physical systems[END_REF] serves as a coordination language for model-based design of distributed real-time embedded systems. It extends the discrete-event model of computation with a carefully chosen relationship between real time and model time. PTIDES provides a framework for exploring a family of execution strategies for distributed embedded systems so that it can directly confront the multiform nature of time in distributed systems. Simulations of it can simultaneously have many time lines, with events that are logically or physically placed on these time lines. As far as we know, they have some semantics for the interactions between events to model the communications of distributed systems. However, we need more mature communication mechanism like asynchronous communication, broadcasting, as well as more compatible way of modeling system, which are not yet supported in PTIDES.

Timed Petri nets (TdPNs) [26] is one of several mathematical modeling languages for the description of distributed systems. It is widely used for the modeling and analysis of concurrent systems with time-dependent behaviour like communication systems. It includes a set of directed bipartite graphs, in which the nodes represent transitions (i.e. events that may occur, signified by bars) and places (i.e. conditions, signified by circles). The directed arcs describe which places are preand/or post-conditions for which transitions (signified by arrows). Each arc associates with an interval (or bag of intervals). In TdPNs, each token has an age. This age is initially set to a value belonging to the interval of the arc which has produced it or set to zero if it belongs to the initial marking. Afterwards, ages of tokens evolve synchronously with time. A transition may be fired if tokens with age belonging to the intervals of its input arcs may be found in the current configuration. Compare to timed Petri nets we use a total different way by means of label transition system (LTS) to model the system behaviour. Our model graph comprises some number of states, with arcs between them labeled by activities of the system. We choose to model our system by means of action based LTS because: 1) our goal is to check the correctness of system communication behaviour, not to verify the correctness of programming computations. So we hide the unnecessary detail information like state variables, and just highlight the information that related to communication behaviour like actions. 2) By this way, we can easily model our system in a compact and hierarchical way since the action based LTS do not show the details information of states (each state is an abstract node).

Spatio-temporal consistence language (STeC) [27], provides a location-triggered specification as well as operational semantics and denotational semantics [28] for describing distributed system with time and location constraints. Syntax and semantics of the language have been proposed to address the issue of spatial-temporal consistence for real-time systems. The language specifies the time and location constrains for each action, and then computes the execution time of processes. However, since our model mainly focus on time properties, we set the information as parameters that are sent by physical part of our system. Typically, in our use-case we sometimes need check car's locations, but such data is not treated at the same level as time information. This is quite different from what the STeC does by adding location constrains. This way, we can separate our model from physical part of system and focus on modeling the communication behaviour of Cyber part. These previous efforts are important since they provide crucial insights on building the timed-model for real-time systems, or contribute to mechanisms and strategies that can be used to model our system.

Conclusion

This paper proposed a flexible time-related behavioural semantic model (called timed-pNets) for modeling communication behaviours of distributed systems. This model is able to build a hierarchical tree structure by composing the components of the systems. The refinement and compatibility of the timed-pNets are considered in the paper. A concrete example throughout the paper is given to represent how to build hierarchical specifications and how to refine them. In the end, we use the TimeSquare tool to check the compatibility of the refined system. Three advantages are implied in our model: first, by introducing logical clock relations, timed-pNets are able to specify the system time-related communication behaviour constrains without relying on a physical common clock; second, by using timed specifications, our model is easy to be composed and has the capability of building a hierarchical structure; the last but not the least, timed-pNets can model the heterogeneous systems including synchronous and asynchronous communications by taking advantage of channels. We believe that the timed-pNets are helpful for analyzing the time-related behaviours of distributed systems including cyber physical systems.

However, since our timed specifications include only two relations (coincidence and precedence), they are not simple to specify some system behaviours like choice. This paper is the foundation for our model, and we are working on the next step, including logical compositions of timed specifications and time bound analysis. Besides, a natural question arises about the scalability and the efficacy of the proposed analysis approach on larger case studies. In our future work, we plan to apply the proposed analysis techniques on larger case studies and check the scalability. We also plan to write a tool to automatically generate timed specifications and check its performance.

Apart from the compatibilities, our model can also be used to check the logical correctness properties. But more interesting properties are time properties such as deadline property that expresses whether system communications can be successfully finished before a certain deadline. To check this property, we shall choose a reference clock and specify the delay constrains in terms of the reference clock. In this paper, even though we define delay variables for actions, we do not provide a way to specify delay constrains here, because it is not a main topic for this paper. In our future work we will extend the model for specifying the delay constrains and check system time properties. Furthermore, we plan to extend the current model timed-pNets to a new duration-pNets so that we can describe the system behaviours whose executions take time. It also looks interesting to translate our model to boolean automata to verify the system properties.

Fig. 1

 1 Fig. 1 Timed-pNets tree structure

Fig. 3 Fig. 4

 34 Fig. 3 Count the delay t α i when C α is an independent clock

••

  The relation 'C α = C β ' (C α coincides with C β ) describes the strict synchronization of clocks. It means that the occurrence of C α appears if and only if the occurrence of C β appears. In other words, the two clocks are synchronized. Formally, C α = C β = ∀i ∈ N, (α_i ≡ β_i) (shown in Fig. 5(a)). This operator can naturally be used to describe synchronous communications. The relation 'C α ≺ C β ' (C α precedes C β ) describes the precedence relation of clocks. It says that the action β from the clock C β cannot occur until the corresponding action α in the clock C α occurs. In other words, clock C α ticks always earlier than clock C β . Formally C α ≺ C β = ∀i ∈ N, (α_i ≺ β_i). As shown in Fig. 5(b), the ith occurrence of the clock C α always appears earlier than the ith occurrence of the clock C β . The relation usually relates to the causalities induced by asynchronous communications.

Fig. 5

 5 Fig. 5 Clock relations. (a) [C α = C β ] = ∀i ∈ N, (α i ≡ β i ); (b) [C α ≺ C β ] = ∀i ∈ N, (α i ≺ β i )

Proposition 1 (

 1 properties of the coincidence relation '=') Given a set of clocks C. The relation '=' on the set C is reflexive, symmetric and transitive. Proof This follows from the fact that ≡ is an equivalence relation on timed-action occurrences. 1) Choose any clock C α ∈ C. Let the ith (i ∈ N) occurrence be α_i. The occurrence α coincides with itself (C α = C α ). So we know the coincidence relation is reflexive. 2) Now choose another clock C β ∈ C. If we have the relation of C α = C β , then we know that ∀i ∈ N, α_i ≡ β_i, which means the action α occurs if and only if the action β occurs. According to the symmetric relation of the operator "≡", we know that the action β occurs if and only if the action α occurs. So we have ∀i ∈ N, β_i ≡ α_i (C β = C α ). Thus the coincidence relation is symmetric. 3) Choose another clock C γ ∈ C. If we have relation C α = C β and C β = C γ , then ∀i ∈ N, α_i ≡ β_i ∧ β_i ≡ γ_i. From the transitivity relation of "≡", we infer ∀i ∈ N, α_i ≡ γ_i (C α = C γ ). Thus the coincidence relation is transitive. Proposition 2 (the properties of precedence relation '≺') Given a clock set C. The relation '≺' on the set C is transitive, but not reflexive, not symmetric. This follows from the same properties on the relation ≺ on occurrences. The proofs are similar to those of Proposition 1. Proposition 3 (substitutivity of "=") Given four clocks C α , C β , C γ , C η which are built on the timed-action α, β, γ and η separately. Let C α = C β and C γ = C η . If C α ≺ C γ , then we have C β ≺ C η . Proof According to the coincidence definition, C α = C β ⇒ ∀i, α_i ≡ β_i, and

Fig. 6

 6 Fig. 6 Timed-pNets: communication behaviour model of cars insertion scenario

Definition 9 (

 9 saturated relation set) Let T S = C, R be a timed specification with a set of clocks C and a set of relations R. The saturated relation set (denoted as R + ) is the clock relation set R augmented by all relations possibly deduced from R, by transitivity of precedence and reflexivity, symmetry, and transitivity of coincidence. For example, if R = {C 1 ≺ C 2 ≺ C 3 } (C 1 , C 2 , C 3 ∈ C), then according to the transitivity property of the relation ≺, we can get the saturated relation set R

Fig. 11

 11 Fig. 11 Steps for generating the TS of a timed-pLTS

apply case 1 )

 1 , a), b) and III) rules else apply case 2), a), b) and II) rules end if else if s i = s 0 then apply case (1), a), b), I) and III) rules else apply case (2), a), b), I) and II) rules end if end if end for end for corresponding occurrence relation and index increase function deduced from the corresponding rule.

Fig. 12

 12 Fig. 12 Simplification of CommIni component

Algorithm 2

 2 Unfold occurrence relation tableInput: A symbolic occurrence table with a clock set C with n clocks.C = {C 1 , C 2 , . . . C n } Output: enumerate occurrence relations of N rounds in the matrix R[j][r],in which j is the index of rows and r is the index of columns (rounds).for eachCi do Indexo f (C i ) := 0 {initialisation} end for set var j, r :=0 var s := s 0 set var C α := anyone from PreAct(s) set var C β := one from PostAct(s) that satisfies a certain guard set var s ← {s |s Cα --→ s} set var s ← {s |s C β --→ s } while r N do while C ∅ do if s = s 0 then r + +; j := 0 end if for each row in table do

Case 3

 3 If the global clock C a g1 and C a g2 are generated from the synchronous vectors . . . , C β 1 , . . . → C a g1 and . . . , C β 2 , . . . , C γ 1 , . . . → C a g2 as shown in Fig. 13(c) then:

1 )V . 1 )

 11 both global clocks are generated by binary communication; 2) one global clock is generated by binary communication and another one is generated by visibility; 3) both global clocks are generated by visibility. Now we analyze the three situations one by one. Given timed-pNets T -pNets= P, A G , C G , J, A J , C J , R J , -→ Let . . . , C α , . . . , C β → C g1 and . . . , C γ , . . . , C η → C g2 (C α , C β , C γ , C η ∈ C J )be two synchronous vectors generating the global clocks C g1 and C g2 . Obviously the four local clocks C α , C β , C γ ,C η cannot be in one hole since the synchronous vectors build binary communications between holes. If the four local clocks come from two holes, then the possible combinations are C α and C γ are in one hole, the other two are in another hole. Or C α and C η are in one hole, the other two are in another hole. The case 1 of the Theorem 2 covers the both situations. If the four local clocks come from three holes, then any two local clocks that come from different synchronous vectors must be in one hole, and the rest two local clocks are in other two different holes. For example, C α and C γ are in one hole, the other two are in other two holes separately. The Case 2 of the Theorem 2 covers the situation. Furthermore, the four local clocks cannot be in four holes (or more than four holes), otherwise there is no local clock relations in R J can be used to deduce global clock relations, so no direct clock relation can be built between C g1 and C g2 . 2) Let . . . , C α , . . . , C β → C g1 and . . . , C γ , . . . , → C g2 (C α , C β , C γ ∈ C J ) be two synchronous vectors to generate the global clocks C g1 and C g2 . Similar to the proof in the previous situation, the three local clocks cannot be in one hole and cannot be in three holes or more. So the only possible combination is that C γ and C α (or C β ) are in the same hole. The rest one is in another hole. The case 3 of the theorem 2 covers the situation. 3) Let . . . , C α , . . . , → C g1 and . . . , C γ , . . . , → C g2 (C α , C γ ∈ C J ) be two synchronous vectors to generate the global clocks C g1 and C g2 . The two local clocks cannot be in two different holes, otherwise there is no local relation can be find between them. So the only possible situation is that the two local clocks are in the same hole. The Case 4 of the Theorem 2 covers the situation. In conclusion, if the relation of two global clock C g1 , C g2 ∈ C G can be deduced by the local clock relations from R J , they must belong to one of the four cases of theorem 2.

Fig. 14

 14 Fig. 14 Layered structure

Fig. 15

 15 Fig. 15 Property checking by TimeSquare

Fig. 16

 16 Fig.[START_REF] Bulirsch | Introduction to Numerical Analysis[END_REF] System specification checking

  Obviously, the updated implementation of hole CommIni is compatible with the abstract timed specification of this hole T S {CommIni} since we have T S {CommIni} T S {U pdatedCommIni} . And the same to the other two holes CommRes[m] since we have T S {CommRes[m]} T S {U pdatedCommRes[m]} .• Result of simulation 2: by simulation, we found violations as shown in Fig.17

  .

Fig. 17

 17 Fig. 17Conflict Detected

Fig. 18

 18 Fig. 18 System specification checking

  26. Valero Ruiz V, Frutos Escrig d D, Cuartero Gomez F. On nondecidability of reachability for timed-arc petri nets. In: Proceedings of the 8th International Workshop on Petri Nets and Performance Models. 1999, 188-196 27. Chen Y. Stec: a location-triggered specification language for real-time systems. In: Proceedings of the ISORC Workshops. 2012, 1-6 28. Wu H, Chen Y, Zhang M. On denotational semantics of spatialtemporal consistency language-stec. In: Proceedings of the 2013 International Symposium on Theoretical Aspects of Software Engineering. 2013, 113-120 Yanwen Chen is a PhD student registed both in the East China Normal University and in the University de Nice Sophia Antipolis. She got her MS degree in both universities in the domain of computer science. Her research interests include distributed systems, cloud computing and formal methods. Now her research topic concerns the formal modeling and real-time scheduling of Cyber Physical Systems. Yixiang Chen is a full professor for computer science and technology at Software Engineering Institute (SEI), East China Normal University (ECNU), where he is coordinating trustworthy software, Internet of things and cloud computing related research activities. Professor Chen is the director of the Engineering Research Cen-ter for Software/Hardware Co-design Technology and Application, MoE of China. He is Member of the Cloud Computing Experts Association of Chinese Institute of Electronics and Vice Chair of Shanghai Pudong IoT Alliance. Eric Madelaine is a senior researcher at INRIA in Sophia-Antipolis, France. He has a diploma from Ecole Polytechnique, Paris, a PhD thesis from university of Paris 7, and an Habilitation from university of Nice. His research interests range from semantics of programming languages, distributed and cloud computing, componentbased software, formal methods, methods and tools for specification and verification of complex programs. He has served in many international conferences committees, including Euromicro, FESCA, SEAA, FMCO, and FACS.

Table 1

 1 Time assignment for the timed-pLTS "Car.CommIni"

	State	Transition	Occurrence relations	Index assignment

Table 2

 2 Steps 2-4: Unfold rounds, generalize, and deduce clock relations

	1st round	2nd round	3rd round	sth round	. . .	Clock relations

Case 1

 1 If the global clocks C a g1 and C a g2 are generated from synchronous vectors . . . , C α 1 , . . . , C β 1 , . . . → C a g1 and . . . , C α 2 , . . . , C β 2 , . . . → C a g2 , which are related to two holes C H α and C H β as shown in Fig.

  is found. If the global clock C a g1 and C a g2 are generated from the synchronous vectors . . . , C β 1 , . . . , C γ 1 → C a g1 and C α 1 , C β 2 , . . . , . . . → C a g2 , which are related to three holes C H α , C H β and C H γ as shown in Fig. 13(b), then:

	Case 2

  So using the substitutivity of = w.r.t. ≺, we get the relation C a g1 ≺ C a g2 . From the two synchronous vectors . . . , C β 1 , . . . , C γ 1 → C a g1 and C α 1 , C β 2 , . . . , . . . → C a g2 , we know that

	Case 2

[START_REF] Fidge | Logical time in distributed computing systems[END_REF] where "-" represents a single hole that does not participate in this synchronization

Acknowledgements This work was partially funded by the INRIA Associated Team DAESD between INRIA and ECNU; by NSFC (61321064 and 61370100); by Shanghai Knowledge Service Platform Project (ZF1213). And we give great thanks to Frederic Mallet and Julien 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.