Functional safety verification and performance measurement of train-train communication link

LIN Junting， XU Qian， CHEN Yong

(1. School of Automation and Electrical Engineering， Lanzhou Jiaotong University， Lanzhou 730070, China；2. School of Electronic and Information Engineering， Lanzhou Jiaotong University， Lanzhou 730070， China)

Abstract： The short-range wireless communication technology has advanced considerably and provides the feasibility of train-train (T2T) communication link in the communication-based train control system. The introduction of the T2T link would reduce the headway and improve operational efficiency. Formal methods are system design techniques that use rigorously specified mathematical models to ensure all behaviors work as expected. And it is exactly the functional safety verification needed. Therefore, to deal with the functional safety verification of the T2T link, an untimed colored petri net model is first constructed. Secondly, the verification process is performed. Conclusions can be drawn from the state space report and the computation tree logic queries. Lastly, the model is parameterized, and then data log files are obtained for further performance measurement. Results show that the proposed criteria are satisfied and there are no defects in the basic design requirements. The transmission delay has considered the reconnection, transmission errors and the interruption. The probability of the delay lower than 150 ms accounts for 98.106%, which meets the specification and the previous field test.

Key words： functional safety； formal methods； colored Petri net (CPN)； state space analysis； performance measurement

0 Introduction

Communication-based train control (CBTC) system is the mainstream signaling system in metro lines. The traditional CBTC system is ground-centric. Movement authority is transferred from the zone controller to trains. There was no direct train-train (T2T) communication link. Studies on the addition of T2T represent a growing field. T2T was initially designed for the train collision-avoidance system only for emergency scenarios[1-2]. In recent years, the train-centric CBTC system[3-4]is proposed and under development. T2T has brought more concerns. Urbalis Fluence[5]offered by Alstom was the first solution. It regards the T2T link as the main access that simplifies the wayside facilities.

A high performance, safe and stable T2T link is urgent to be verified. Device-device (D2D) technique provides the technical support for the T2T link. Ref.[6] modeled the long term evolution-for metro (LTE-M) with deterministic and stochastic Petri nets to evaluate the system reliability. Ref.[7] utilized the stochastic network calculus method to evaluate the D2D performance for high-speed railway.

Along with the software-intensive systems become popular, the traditional fail-safe concept is transformed into a generalized safety concept with probabilistic characteristics, and the safety goal is altered into functional safety. Functional safety is defined as part of the overall safety and depends on the functional physical units operating correctly in response to their inputs. Essentially, it is reflected by the functional control logic of the system design. Ref.[8] reviewed the formal method in the trustworthy construction of CBTC. Formal methods have rigorous mathematical specifications that allow getting rid of ambiguities, and the mathematical proof covers the possible behaviors exhaustively whereas tests are only samples.

Colored Petri net (CPN) is a discrete-event formal modeling language, which integrates the classic Petri nets with the functional programming language[9]. CPN has been applied in the field of reliability and safety engineering. Ref.[10] performed the scenario modeling of a satellite-based train control system by CPN. So did the safety communication protocol in Ref.[11], the reliability of the train-ground data communication system in Ref.[12], and the hazard identification of temporary speed restriction scenarios in Ref.[13]. Inspired by the former literatures, this paper intend to implement the functional safety verification and performance measurement of the T2T link by CPN and CPN-Tools.

In this paper, firsly, whether D2D is feasible for providing the T2T link is analyzed, and a brief introduction of CPN is gived. Secondly, a non-timed CPN model of the T2T link is constructed. Interaction simulation is used to check the syntactic and semantic errors. Thirdly, to perform the functional safety verification, we verify the standard properties shared by all CPN models and the specific properties proposed for our subject. Finally, to perform performance measurement, the corresponding monitors are available for collecting data.

1 Feasibility analysis of T2T implemented by D2D technique

D2D makes the adjacent terminals directly communicate without base stations. D2D supports the internet of things. One of the typical scenarios is vehicle-to-vehicle (V2V) communication in the intelligent transportation field.As the increasing application of LTE-M, D2D offers the potential technical support for the T2T link in metro lines. The metro operation pursuits to shorten the headway at relatively low speed (80 km/h-120 km/h). According to Ref.[14], for a train with a weight of 330 t at the initial speed of 80 km/h, the braking distance is 400 m. The detection range of D2D is from 10 m-1 000 m, which meets the regular braking distance. Additionally, D2D can achieve a maximum data rate of 1 Gb/s that can satisfy the information load demands.

In the train-centric CBTC, the establishment of the T2T link is based on the front train recognition. So the process of front train recognition here is assumed to have already taken place. Besides, the allocation of channel resources and power control is critical and generally researched by other simulation methods, so they are not taken into account in the model construction. As can be seen from Fig.1, the message sequence chart of the T2T link achieved by D2D is proposed as a modeling basis. The local train sends the detecting request. Once there are trains in front of the local train and the front train recognition has taken place, the local train would keep real-time communication with the front train.

Fig.1 Message sequence chart of T2T link

2 Model of T2T link with CPN

2.1 Colored Petri net

The formal definition of the non-hierarchical CPN introduced in Ref.[9] is presented in Eq.(1).

CPN=(P,T,A,∑,V,C,G,E,I).

(1)

1) Tuples related to the places

Pis a finite set of places. Places drawn as ellipses are used to represent the state of the system to be analyzed. Places are marked with some tokens (shown in a small green circle) and each token is attached with a data value called the token color. The tokens on a specific place constitute the marking of that place.

∑ is a finite set of non-empty color sets. The finite set of token colors depends on the types of places called color set.

C:P→∑ is a color set function that assigns a color set to each place;

I:P→EXPRφis an initialization function that assigns an initialization expression to each placep.

2) Tuples related to the transitions

Tis a finite set of transitions. Transitions drawn as rectangular boxes represent the occurring events. The inscriptions of the transition are used to manipulate and select the tokens that can be move around. When a transition is enabled, it removes the tokens from its input places and adds them to its output places.

G:A→EXPRVis a guard function that assigns a guard to each transitiont;

3) Tuples related to the arcs

Arepresents a finite set of directed arcs.A∈P∩T=P∩A=φ;

E:A→EXPRVis an arc expression function that assigns an arc expression to each arcasuch thatType[E(a)] =C(p)MS, wherepis the place connected to the arca;

Vis a finite set of typed variables thatType[v] ∈∑ for all variablesv∈V.

2.2 Non-timed CPN models for T2T link

CPN Tools is a software for editing, simulating and analyzing CPN models. Color sets and variables are declared as depicted in Fig.2. The color sets are of enumerate type with the keyword “with”. Status is used to describe the four states, i.e., IDLE (the initial state where the local train is not connected), WAIT (the local train is waiting to connect with the front train), SR (the local train sends the link request), FR (feedback response). PACK is used to specify the three states of the T2T link. “FULL” represents that the packets are transmitted completely. “PART” represents that the packet is lost partially or disordered. “NULL” represents all packet is lost. The result would reflect whether the link is established or not. Variables belong to the specified color set.

Fig.2 Declarations of color sets and variables

The CPN model of the T2T link is demonstrated in Fig.3. Tokens can flow within the net structures to model dynamic behaviors. Via the simulator in CPN tools, accuracy can be checked.

Fig.3 CPN model of T2T communication link

1) The left part of the model is to detect whether the front trains are ahead of the planned route. The tokens are transmitted from the place SystemStatus to the transition Start to detect. Detecting results are reflected by the place Detecting Results. The arc expression of the one branch is“1`SUCCESS”, indicating there are probably trains ahead of the route. The other branch is “1`FAIL”, indicating there is no front train. Given the transition Detected is enabled, the tokens would be transferred into the place Connect Reliable. Arc expression is “1`SUCCESS” by default.

2) The middle part is to model the status of the on-board wireless communication system. The output and input arc expressions of the transition Online are both “1`SUCCESS”, which indicates that the tokens can flow to the place Connected. Consequently, the place SystemStatus changes from “WAIT” to “SR”. The transition Send Request is fired, and the local train sends a link request to its front train.

3) The right part is to model the data transmission. The local train’s transmitter (represented by the place Transmitter 1) transmits the “MSG” to the front train’s receiver (represented by the place Receiver 2). Furthermore, the state of the link is set to be full (represented by the transition Full_trans). Then the front train confirms (represented by the transition Acknowledge). The link state of the front train to the local train is set to be random. The front train’s transmitter (represented by the Transmitter 2) sends the response to the local train. In general, there is a 3-way handshake key agreement protocol with message authentication and a period key-updating protocol in the data transmission procedure.

4) Thenormal transmission (represented by transition Full_trans_1), the completely lost (by Data_full_loss) and the partially lost (by Data_part_loss&Error) are separately connected with the transitions Distance Updated, Feedback Results and Link Reconnect after Interruption. Taken the condition that the data is partially lost as an example, the token on the place Receiver1 is “1`PART”, and then it is transferred into the transition Feedback Results. One branch is to reflect its state to place Connected. The other branch is to place SystemStatus. Then the results are transferred to the transition Feedback Results.

Both the simulation and testing of a CPN model are implemented by model execution. It is found that the token flow accurately in the net structure. Simulation is suitable for detecting errors and obtaining increased confidence in the correctness of a system. However, since it cannot be guaranteed that the simulations cover all possible executions, so it cannot be used to ensure this with 100% certainty. Therefore, the state-space analysis, one of the formal analysis methods, is performed in the following section.

3 Functional safety verification

3.1 Verification of standard properties

State space covers all possible executions of the system under consideration. It can be used to verify, i.e., prove in the mathematical sense that the system possesses a certain formally specified property.

Through the state space calculator from CPN-Tools, the standard state-space report is generated. Statistics are shown in Fig.4.

Fig.4 Statistics of CPN model

Status “Full” manifests that all available states in the state space are calculated. There are 16 nodes and 19 arcs, where the nodes correspond to the set of reachable markings while the arcs correspond to occurring binding elements. A strongly-connected-components graph (SCC graph) is derived from the graph structure of the state space. The nodes in the SCC graph are subgraphs, called strongly connected components (SCCs), and are obtained by making a disjoint division of the nodes in the state space such that two nodes are in the same SCC if and only if they are mutually reachable. The model has one node in terms of SCC Graph.

Fig.5 is a complete reachability graph of the model in Fig.3. A node descriptor in the rectangle shows the nodes’ markings, whose format is “PageName `PlaceName 1:token”. Similarly, an arc descriptor describes the binding element associated with the arc, whose format is “ArcNumber: NodeName-> NodeName PageName `TransitionName 1:{ }”.

Fig.5 Reachability graph of overall model

A home marking can be reached from any reachable marking. Home properties show that all markings are home markings. The results are desirable because there is one node in SCCs graph that all nodes (represent the marking) are mutually reachable.

Liveness properties express that there are none dead markings and one dead transition instance (transition Offline). The rest of the transitions are “l(fā)ive”. Dead markings reflect the termination of the system operation and the unavailability of further subsequent actions. Dead transitions refer to the transitions that do not appear in any of the binding elements. As seen from Fig.7, there are none dead markings, which means that the model would not be terminated in the finite number of simulation steps. It also means the D2D radio set would not be offline that explains why the transition Offline is dead.

Fig.6 Home properties and liveness properties

Fig.7 Liveness properties

The fairness properties give information about how often transitions occur in infinite occurrence sequences. As shown in Fig.7, the impartial transition instance is none. A transition is impartial if it occurs infinitely often in all infinite occurrence sequences. Therefore, the results show there are no infinite occurrence sequences, which is desirable as expected.

3.2 Verification of specific properties

Common design flaws can be excluded by those standard properties, such as no deadlock, live-lock. Other properties also need to be investigated aimed at the target problems of the specific application.

Criterion 1: The system to be analyzed is required to work in a particular state. The criterion reflected in the CPN model is that there is always only one token in the place SystemStatus.

It is verified by the boundedness shown in Fig.8. The best upper integer bound of a place specifies the maximal number of tokens that can reside on that place in any reachable marking. The best upper bound integer indicates that the maximum number of tokens in the place SystemStatus is one. So is the best lower bound integer. Therefore, it can be summarized that the model’s operation meets the expected behavior.

Fig.8 Best integer bounds

Criterion 2: After the connection link is established, the distance information shall be updated timely, i.e., verify whether a certain state of the system can turn into a required state and find which of transitions can trigger it. It is a fundamental feature of functional safety verification. The criterion reflected in the CPN model is that the relevant nodes containing token “1`SR” are found.

SearchNodes is the primary function traversing the state space. PredNodes and EvalNodes are the abbreviations of SearchNodes functions. Analogously, SearchArcs, PredArcs and EvalArcs traverse the arcs of the state space. Computation tree logic (CTL) queries are written as Fig.9.

Fig.9 Queries for criterion 2

“Operation (SR)” returns to all the nodes with token “1`SR”. Parallel arcs that can be transferred from other nodes to that node also need to be enumerated.

The “Evaluate ML” tool is used to evaluate the queries and the results are shown in Fig.10. It is found that node 6 contains the required “1`SR” (sends the communication request). Three parallel arcs, i.e., arc 18, arc 17, arc 6, are connected to node 6.

Fig.10 Queries results of criterion 2

As Fig.11 depicted, details of the nodes and marking can be further obtained. By “display a partial SS” tool, node 6 is first obtained and then its predecessors and successors. Node 6 has the form as 3∶1, i.e., the number of predecessors and successors. Consequently, its predecessors (node 15, node 14, node 5) and its successor (node 7) are obtained. From Fig.11, the token “1 `SR” can be sent from the transition Feedback Results (node 15), Distance Updated (node 14) and Online (node 5).

Fig.11 Fragment of reachability graph for criterion 2

Criterion 3: Once the disconnection occurs, the system should attempt to re-establish the connection and continue to detect the front train. The criterion reflected in the CPN model is that judge whether a particular state can be transferred to another. More specifically, after the Receiver1 obtains the token “1`NULL” (meaning that the link breaks down), it should be judged whether the place SystemStatus turns into “1`SR” (Send the request).

The CTL queries achieve the above purpose shown in Fig.12. We defined the function “Dataloss” for the place Receiver1 and the function “Operating” for the place SystemStatus. “List.nth(Dataloss(NULL),0)” is the function for the variable Source (represents the source node), which will return to the node where place Receiver1 has the token “1`NULL”. Meanwhile, the variable Target (represents the target node) node returns to the node where the SystemStatus has “1`SR”.

Fig.12 Queries for criterion 3

The results are shown in Fig.13.

Fig.13 Queries results for criterion 3

The path from the source node 16 to the target node 6 is [16,1,3,5,6]. Besides, as depicted in Fig.14, node 16 has the marking “Receiver1∶1`NULL” and node 1 has the markings “Connected 1∶1`FAIL” and “SystemStatus 1∶1`IDLE”. Therefore, we verify the occasion where the Receiver1 receives no more data causing the link to break down and the system return to idle. Node 3 has themarkings “Detecting_Results:1`SUCCESS” and “Connected 1∶1`FAIL”. Similarly, node 1 has the markings “Connect_Reliable: 1`SUCCESS” and “Connected 1∶1`FAIL”. Node 6 has “SystemStatus 1∶1`SR” and “Connected:1`SUCCESS”. The above information proves that after re-establish the connection by the transition Reconnect, the communication link is available.

Fig.14 Fragment of reachability graph for criterion 3

4 Performance measurement

Timed CPN is used for simulation-based performance analysis, whose basic idea is to conduct lengthy simulations of a CPN model, during which data is collected from the occurring binding elements and the markings reached in order to calculate estimates of performance measures of the system. Monitors implement the above features.

As shown in Fig.15, the four functions of the monitors are to define how monitors operate. Here we use the“DataPacketDelay” whose type is data collection. The “Predicate” function determines when to collect data. If the predicate function evaluates to be true, the “Observer” function determines which data to collect. The “Start” function aims at collecting data from the initial identification. “Stop” function is used for collecting data from the final marking.

Fig.15 Four functions of the monitors

According to Ref.[15], the transitions’ delay obeys the exponential distribution. The probability density functionf(x) and the cumulative distribution functionF(x) are exponential distribution and calculated by

f(x)=λe-λx,

(2)

F(x)=1-λe-λx.

(3)

Time constraints of the transitions are calculated, considering the following circumstances:

1) Delay caused by reconnection: when the place SystemStatus holds the token 1 `IDLE again, the system attempts to re-establish the T2T link. It is assumed that if there is no response within 3 seconds before detection, i.e., the timestamp of transition No Response is“@+300”, the connection is re-established that transition Reconnect is enabled. It is important to note that the model’s unit is milliseconds, and we should transfer the seconds into milliseconds.

According to the QoS requirement from Ref.[15], the probability of end-to-end transmission delay lower than 150 ms accounts for more than 98%. The value ofλreconnectis determined as

p=1-e-λrx,

(4)

(5)

2) Delay caused by transmission errors means that no data is available to update the distance during transmission error until the data packets are completely received.

It is stipulated that the periods of transmission interference areT<0.8 s (95%) andT<1 s (99%) from Ref.[15]. The period should be as short as possible to improve the simulations’ accuracy. So theT<0.8 s (95%) is chosen andλerroris valued by

(6)

3) The probability of the interruption time no more than 2 s accounts for lower than 99.92% in the LTE-M single network communication.

Therefore,

(7)

The timed CPN model is shown in Fig.16, where “@+round(1 000*exponential(3.565 4)” means that the transition Data_part_loss&Error is enabled and the delay obeys the parameter 3.565 4 of the exponential distribution.

Fig.16 Timed CPN model of T2T communication link

Through the parameters valued by the transitions, the 200 000 ms simulation is carried out. Data logs files of the Receiver1 data collection monitor are obtained. Part content is captured shown in Fig.17, which has four columns. The “data” and “time” columns are abstracted and drawn shown in Fig.18 in Table 1, statistics reveal that the delay less than 150 ms is accounted for 98.106%, which meets the specification in Ref.[15] that point out the end-to-end delay lower than 150 ms accounts for≥98%. Statistics also meet the results from theoretical derivation in Ref.[16] and field test in Ref.[17].

Fig.17 Screenshot of data log file

Fig.18 Diagram of delay results

Table 1 Statistic results

5 Conclusions

The main idea of formal methods is to represent the system’s behavior and its desired properties in appropriate logical frameworks and develop a relationship between these two by mathematical reasoning or rigorous state exploration techniques. Our work intends to deal with the T2T link from the perspective of functional safety verification and performance measurement.

1) In terms of the communication medium, the T2T link’s feasibility implemented by the D2D technique is analyzed. Factors are taken into consideration, such as braking distance, D2D detecting range and information load capacity. The establishment procedure is given in the message sequence chart.

2) A non-timed CPN model of the T2T link is constructed. The syntactic and semantic errors have been checked. The model is available for further analysis.

3) The standard properties and the specific properties are checked for functional safety verification. On the one hand, the standard properties are desirable, such as the statistic, home properties, liveness properties and fairness properties. On the other hand, the three criteria are satisfied, i.e., ensuring all reachable states, markings and sequences satisfy the given prediction. The fragments of the state space inspect the individual states and events.

4) Simulation-based performance analysis is performed by the model parameterization. Three circumstances are taken into consideration, i.e., the reconnection, transmission errors and interruption. After analyzing the statistic, it is proven that the statistics meet requirements from specification and field tests.