Content area
With the development of automatic control and communication technology, communication-based train control system is adopted by more and more urban mass transit system to automatically supervise the train speed to follow a desired trajectory. Taking reliability, availability, maintainability, and safety into consideration, 2 × 2-out-of-2 safety computer platform is usually utilized as the hardware platform of safety-critical subsystem in communication-based train control. To enhance the safety integrity level of safety computer platform, safety-related logics have to be verified before integrating them into practical systems. Therefore, a significant problem of developing safety computer platform is how to guarantee that system behaviors will satisfy the function requirements as well as responding to external events and processes within the limit of right time. Based on the qualitative and quantitative analysis of function and timing characteristics, this article introduces a formal modeling and verification approach for this real-time system. In the proposed method, timed automata network model for 2 × 2-out-of-2 safety computer platform is built, and system requirements are specified and formalized as computation tree logic properties which can be verified by UPPAAL model checker.
Introduction
With the rapidly growing of passenger flow in big city, communication-based train control (CBTC) system is believed to be the chief choice for urban railway transportation system. As an emerging new technology, CBTC overcomes the fundamental limitations of conventional track circuit-based railway signal systems and employs continuous, high capacity, bidirectional train-to-wayside data communications to realize high-resolution train location determination. Therefore, train-borne and wayside processors are capable of permitting more effective utilization of the transit infrastructure and implementing a series of vital functions.[1],[2] Taking reliability, availability, maintainability, and safety into consideration, 2 × 2-out-of-2 safety computers are adopted as hardware platforms by more and more safety-critical subsystems in CBTC such as zone controller (ZC) subsystem, data storage unit (DSU) subsystem, computer interlocking (CI) subsystem, and so on.
To copy with the increasingly exacting performance demands in real-time control system,[3]-[6] the architecture and functions of safety computer platform are becoming more and more complex. As a result, the task of verifying that these real-time applications are able to satisfy their timing requirements is more critical and difficult today than ever before. It is believed that analyzing and verifying system performance based on design model is a principal means to ensure the security and reliability of the real-time system.[7] In contrast to classical software engineering measures, model-based development (MBD) is a novel, promising method. MBD supports accurate definition of the system requirements and verification of the designed model in which process formal methods are commonly adopted. Formal methods are mathematics-based techniques, often supported by reasoning tools, which offer a rigorous and effective way to model, design, and analyze computer systems. Rodriguez-Navas and Proenza[8] discussed how computer clocks might influence the temporal behavior of a distributed application and systematically validated the modeling pattern for each type of computer clock. Nemeth and Bartha[9] detailed a formal verification approach for safety procedure of a nuclear power plant written in function block diagram (FBD) language. The approach is based on the Colored Petri net (CPN) representation and a pre-developed library of CPN subnets to represent the FBD specification in an identical structural way. Mokadem et al.[10] introduced a framework of modeling and verification of a particular timed multi-task programmable logic controller, but this model was constrained with atomicity hypotheses concerning program execution and only the reaction time property was checked. To the limitation of CPN, the real-time property was not considered in this work. Navimipour[11] presented an applicable method for Trustworthy Human Resource Discovery (THRD) in Expert Cloud. A Kripke structure with marked states was defined to provide the formal relationship between the expanded model and the original state diagram structures. The expected properties of the structures and compositions of THRD were described by temporal logic languages and implemented by NuSMV model checker.
Over recent years, the complexity of automatic train control system has increased dramatically. This makes the formalization of safety applications a very difficult task. Formalization is important to verify whether the design could meet the specified safety requirements. Increasing evidences have indicated that formal methods are widely used in railways during the past few years.[12] Cimatti et al.[13] applied model checking techniques and formally verified the "safety logic" of a railway interlocking system. The formal model was structured to retain the reusability and scalability properties of the system being studied. Zhang et al.[14] proposed a formal verification method to describe the safety communication protocols using interface automata (IA). They translated IA model into PROMELA model so that the protocols could be verified by the model checker SPIN. However, this method did not mention how to analyze the deadlocks using the counter example given by SPIN. Ahmad et al.[15] investigated behavior modeling and formal verification of Chinese Train Control System Level-3 using Architectural Analysis and Design Language. Emphasis was paid on how to depict both discrete behavior of the control system and continuous behavior of the train in the movement authority scenario.
In the past decades, a number of efforts have been made in designing and modeling of fail-safe critical system.[16],[17] Ma and Gao[18] designed some key techniques consisting of safe hardware data comparator, high-speed parallel communication buses between two independent channels, and self-diagnosis programs to meet the industrial control requirements. Chen et al.[19] presented a scheme of key algorithms for the vital computer with 2 × 2-out-of-2 structure including task synchronization and data comparison between the 2-out-of-2 processors. The feasibility and validity were proved by the results of laboratory testing. Sreekumar et al.[20] developed an adaptive fault-tolerant scheduling mechanism for a dual redundant avionics mission system. The augmented scheme could achieve full functionality when no fault occurs, as well as providing a fail-safe mechanism for a single fault. With the goal of reducing implementation, saving budget, and accelerating time to market, commercial off-the-shelf (COTS) components have been adopted as an alternative strategy to safety-critical systems. Although practical experiences in these two industries had proven that COTS components were comparable with custom-designed components in terms of performance, efficiency, and reliability, the principal danger posed by the utilization of COTS components in safety-critical applications lied in the discontinuity and uncertainty.[21] Some researchers have done a lot of work on integrating COTS components into safety-critical system in a safe and reliable way.[22]-[24] To our knowledge, most researches on modeling of safety computer platform focus on logical computation correctness and function safety and timing requirements which are also vital to safety-critical control are usually overlooked. Besides, the feasibility and validity of requirement specification are usually not proved until the completion of laboratory testing or real line testing of prototype. It costs more time and money if design defects are found in this process. So theoretical verification is desirable to find the design defects and verify whether some properties are satisfied as early as possible.
This briefly introduces a formal modeling and verification approach for 2 × 2-out-of-2 safety computer platform based on the timed automata (TA) theory.[25] TA are chosen precisely due to the following features. (1) TA are formal description methods with a mathematical basis. (2) They assign a real value to each clock. As time advances, the values of all clocks change, reflecting the elapsed time. (3) They are good at describing transitions from locations to locations with certain timing restrictions. The structure of safety computer platform is analyzed and system function specification and performance specification are retrieved. Then, select the corresponding requirements from the specification document and transform them into TA models through extracting these requirements. Furthermore, FSMU || MP || CP (FMC) timed automata network (TAN) model is built considering timing constraints and action sets between component automata. Function requirements and timing requirements are specified and formalized as computation tree logic (CTL) properties which can be verified by UPPAAL model checker. The verification results illustrate that the proposed method is effective to describe the characteristics of safety computer platform and verify safety, bounded liveness, and timing properties. The structure of this article is as follows. In section "The structure of 2 × 2-out-of-2 safety computer platform," the hierarchical structure of 2 × 2-out-of-2 safety computer platform is illustrated. Section "Formal modeling and verification methodology based on TA" presents the TA theory and outlines the formal modeling and verification approach for such real-time systems. Section "Modeling of 2 × 2-out-of-2 safety computer platform" details the FMC model, and Section "Simulation and verification" explores how to simulate the behaviors of different components in the fail-safe management (FSM) model as well as applying our verification strategy with the UPPAAL model checker. Finally, the article ends with conclusions in section "Conclusion."
The structure of 2 × 2-out-of-2 safety computer platform
The 2 × 2-out-of-2 safety computer platform has a hierarchical structure, and the whole platform can be divided into two independent channels.[22] Two channels running the same logic algorithms are connected by reciprocal status checking line from which working parameters of different channels are exchanged. Each channel consists of two main processors (MPs) and one fail-safe management unit (FSMU), while two communication processors (CPs) are shared by both channels. The two MPs in the same channel are independent computers, connected in parallel to create 2-out-of-2 logic. Every MP can receive input data from both CPs, deal with application program, and send computing results to both CPs. Only if the results from the two MPs are identical, the output data can be sent to outer systems. The CPs which in redundant configuration are responsible for providing interfaces to outer systems for MPs in both channels. In each channel, FSMU continuously supervises the working status of MPs and applies recovery or shutdown procedures when abnormal states are detected. Under normal circumstances, although both channels can execute application, only one channel is selected to transfer its computation results to other systems. The architecture of safety computer platform is shown in [Figure 1].
Figure 1.
Structure of safety computer platform.
[Image omitted: See PDF.]
Formal modeling and verification methodology based on TA
Formal definition of TA
Definition 1
A TA is a tuple [Formula Omitted: See PDF], where L is a set of locations; [Formula Omitted: See PDF] is the initial location; C is the set of clocks; A is set of actions, co-actions, and the internal [Formula Omitted: See PDF] action; [Formula Omitted: See PDF] is a set of edges between locations with an action, a guard and a set of clocks to be reset; B (C ) is the set of conjunctions over clocks; and [Formula Omitted: See PDF] assigns invariants to locations.
Definition 2
(Semantics of TA ). Let [Formula Omitted: See PDF] be a TA. The semantics is defined as a labeled transition system [Formula Omitted: See PDF], where [Formula Omitted: See PDF] is the set of states, [Formula Omitted: See PDF] is the initial state, and [Formula Omitted: See PDF] is the transition relation such that
[Formula Omitted: See PDF]
where for [Formula Omitted: See PDF], [Formula Omitted: See PDF] maps each clock x in C to the value [Formula Omitted: See PDF], and [Formula Omitted: See PDF] denotes the clock valuation which maps each clock in r to 0 and agrees with u over [Formula Omitted: See PDF].
Definition 3
(Semantics of TAN ). Let [Formula Omitted: See PDF] be a network of n TAs. Let [Formula Omitted: See PDF] be the initial location vector. The semantics is defined as a transition system [Formula Omitted: See PDF] where [Formula Omitted: See PDF] is the set of states, [Formula Omitted: See PDF] is the initial state, and [Formula Omitted: See PDF] is the transition relation defined by
[Formula Omitted: See PDF]
UPPAAL
UPPAAL is an integrated tool for modeling, simulation, and verification of real-time systems developed jointly by Aalborg University and Uppsala University. It is appropriate for systems which can be modeled as a collection of non-deterministic processes with finite control structure and real-valued clocks, communicating through channels or shared variables. A system is represented in UPPAAL by a collection of TA. Sending a message is denoted by "!" while receiving the message is denoted by "?." These automata also handle a set of integer variables, a feature which makes it suitable for the modeling of real-time systems with great complexity. Then, a guard is a conjunction of atomic clock conditions and similar conditions on the integer variables. Moreover, a clock reset may be augmented by an update of the integer variables, of the form for some constants.[26]
Modeling and verification approach introduction
As the safety computer platform is a complex real-time system with high safety integrity level (SIL), any formal model specified should include not only the functional aspects of the system but also its temporal behaviors. Considering the characteristics of TA model, we adopt it in the design of safety computer platform. Based on TA model, a discrete automaton is extended with a finite set of real-valued variables, named clocks, to model the passage of time. The complexity of system can be decomposed by TAN. For each processor in [Figure 1], there is a corresponding TA model which describes the function requirements and timing requirements in detail. All the processors in safety computer platform together constitute a TAN which represents the coordination relationship of different parts. So, the constructed TAN is an abstract safety computer platform model, which describes the whole dynamic control process of the system. Moreover, function requirements can be translated to state formulae and path formulae which describe individual state as well as quantifying over paths or traces of the model to represent reachability, safety, and liveness. Time properties can be described by timing restrictions and action sets represented by CTL specification language. Finally, the verification tools, such as UPPAAL verifier, can be used to check whether all locations of the model are reachable for ensuring the completeness of the constructed model. Here, the dangerous states or forbidden states should be excluded. By this way, function characteristics and timing characteristics of the real-time system are verified. If the model contains undesirable state, it should be modified until both function requirements and time properties are satisfied. Detailed steps are shown in [Figure 2].
Figure 2.
Flow diagram of modeling and verification.
[Image omitted: See PDF.]
Modeling of 2 × 2-out-of-2 safety computer platform
Function analysis
If we consider one 2-out-of-2 channel as a whole, the entire 2 × 2-out-of-2 safety computer platform can be abstracted as a hot backup system. There are six possible states for each channel including no power state, start state, following state, host state, standby state, and fault state. No power state is the initial state for each channel. When the processors in safety computer platform power up, they will turn to start state at once. Following state is the prerequisite of entering standby mode in which memory information and historical data of the host channel are studied. Besides, the fault state denotes the abnormal condition, where the breakdowns occur in this channel. Possible transitions between different states are shown in [Figure 3].
Figure 3.
State transition diagram.
[Image omitted: See PDF.]
In normal condition, one channel is working in host state, the other one keeps working in standby state. Both channels receive input data from outer systems and execute application computation, but only the channel in host state outputs its computation results by which way the uniqueness of output data is ensured. In order to guarantee the consistency of output data in case of state transition, the standby channel should make sure that its computation results be identical to the host one. Otherwise, the channel in standby mode is supposed to fail to work and should be restored to the fault state. Under this situation, the whole safety computer platform is thought to be in the degraded condition, although it can perform logic computation successfully as well. When one channel is recovered from the fault state, it should enter the following state at first to catch up the history information of the host channel.
In each channel, the MPs work in task-level synchronization state to overcome the flaws of anomalous errors. As a result, each control cycle is divided into small micro-periods including input data exchange and synchronization micro-period, computing micro-period as well as memory comparison and output micro-period. Predetermined time restrictions are assigned to each micro-period. Once violations of time restrictions and other abnormal status such as self-diagnosis abnormal or data comparison errors are detected, FSMU will apply recovery procedure to the fault channel. During recovery process, it still constantly monitors the whole process by allocating fixed timeouts for each recovery process. If one channel is consistently failing, for example, recovery times exceeds a threshold in a given interval, we can conclude that this channel falls into a discontinuity state and permanent fault is assumed to occur. In this situation, the failed channel should be triggered to no power state. Diagnosis and maintenance are needed before it is allowed to restart again. The division of micro-periods is described in [Figure 4].
Figure 4.
Division of micro-periods.
[Image omitted: See PDF.]
Formal modeling
The working procedure of safety computer platform is a typical real-time process. To model real-time systems, TA can be extended with timing constraints and action sets between component automata. Time is continuous and it elapses at the same pace throughout all the TA models.[27] In UPPAAL, the clocks are absorbed to handle time, and transitions are employed to define how the system acts. A system can be modeled as a network of several such TA in parallel. The model is further extended with bounded discrete variables that are parts of the states. A state of the system is defined by the locations of all automata, the clock constraints, and the values of the discrete variables. Every automaton may fire an edge separately or synchronize with another automaton which leads to a new state.
The TAN for 2 × 2-out-of-2 safety computer platform is FMC which contains the following elements: FSMUA, FSMUB, MPA1, MPA2, MPB1, MPB2, CP1, and CP2. FSMUA, MPA1, and MPA2 consist one channel and FSMUB, MPB1 as well as MPB2 consist the other one. CP1 and CP2 are responsible for sending output data to outer systems. FSMU, MP, and CP models are given in [Figures 5]-[7], respectively. In FMC, the symbol "!" denotes a transition signal sending, while the symbol "?" means a transition signal receiving, which can realize the synchronizing transitions between FSMU, MP, and CP models. In the formal abstracting and describing process, the consistency between the requirements and the corresponding FMC model must be ensured. According to Definition 1, FSMU, MP, and CP models are defined as follows:
FSMU model:
State SFSMU = {NoPower, Start,InitSyn, Following, Followed, Host, Standby, HostSync, StandbySync, H_Calculate, S_Calculate, H_CalOK, Fault, S_CalOK, H_OutCmp, H_OutCmpOK, H_StateCmp, H_LoopCon, S_LoopCon, S_OutCmp, S_OutCmpOK, S_StateCmp}.
Initial state [Formula Omitted: See PDF].
Action AFSMU = {powerupA, resetA, poweroffA, selfOKA1, selfOKA2, initsyncA, statefollowA1, synA1, synA2, statefollowA2, followokA, workA, StoHA, synOKA, calculateA1, calculateA2, calOKA, compareA1, compareA2, CmpOKA, powerupB, resetB, poweroffB, selfOKB1, selfOKB2, initsyncB, statefollowB1, statefollowB2, followokB, workB, StoHB, synOKB, synB1, synB2, calculateB1, calculateB2, calOKB, compareB1, compareB2, CmpOKB, StateCmpOK, statedata, stateOK, sLoop}.
MP model:
State SMP = {NoPower, Start, Following, Followed, Host, Standby, StandbySync, H_OutCompareOK, HostSync, S_CalculateOK, H_CalculateOK, S_OutCompareOK}.
Initial state [Formula Omitted: See PDF].
Action AMP = {powerupA, resetA, poweroffA, selfOKA1, selfOKA2, initsyncA, statefollowA1, statefollowA2, followokA, workA, StoHA, synA1, synOKA, calculateA1, calculateA2, calculateOKA, compareA1, compareA2, CompareOKA, powerupB, resetB, synB1, poweroffB, selfOKB2, initsyncB, workB, statefollowB1, statefollowB2, followokB, StoHB, synOKB, calculateB1, calculateB2, calculateOKB, compareB1, compareB2, CompareOKB, sLoop}.
CP model:
State SCP = {NoPower, Start, Working, Pause}.
Initial state [Formula Omitted: See PDF].
Action ACP = {powerupA, resetA, poweroffA, resetB, powerupB, poweroffB}.
Figure 5.
Model of FSMU.
[Image omitted: See PDF.]
Figure 6.
Model of MP.
[Image omitted: See PDF.]
Figure 7.
Model of CP.
[Image omitted: See PDF.]
Function requirements and timing requirements analysis
Relying on above descriptions about system structure and functions, we could derive all the function requirements needed to be verified to guarantee the function correctness and bounded liveness of the safety computer platform. To keep the article concise, only some of the safety-critical properties are listed as shown in [Table 1].
Table 1.
Function requirements.
| Req. ID | Function requirements |
| F1 | There is no deadlock in FMC model |
| F2 | FSMU and MP can work in host or standby state |
| F3 | FMC model can work in hot backup mode |
| F4 | FSMUs and MPs in different channels cannot work in host state at the same time |
| F5 | Once the channel in host state breaks down, the other channel will turn to host state automatically if it is in standby state |
| F6 | FSMU in host mode sends state data to FSMU in standby mode periodically |
| F7 | If FSMU fails more than three times, it will be triggered to no power state |
| F8 | If there is no FSMU in host or standby state, CP cannot be in working state |
FMC: fundamental modeling concepts; FSMU: fail-safe management unit; MP: main processor; CP: communication processor.
Timing requirements reflect the characteristics of the environment in which the system works and expects a response. Because all the kernel applications of FSMU and MP are periodic, we allocate a fixed time to each control cycle. In order to reduce system response time, each control cycle is divided into three micro-periods with different time intervals. At the end of each micro-period, MPs required to inform FSMU the working status. Based on this information, FSMU will judge the synchronization status of MPs in the same channel and decide whether they can proceed to next micro-period. On the basis of either theoretic viewpoints or practical viewpoints, timing requirements are summarized in [Table 2].
Table 2.
Timing requirements.
| Req. ID | Timing requirements |
| T1 | Control cycle of FSMU cannot exceed 400 ms |
| T2 | Data exchange and synchronization micro-period cannot exceed 20 ms |
| T3 | Computing micro-period cannot exceed 280 ms |
| T4 | Memory comparison and output micro-period cannot exceed 40 ms |
| T5 | Synchronous tolerance between MPs in the same channel is no more than 20 ms |
| T6 | Initial synchronization and self-diagnosis time of FSMU cannot exceed 400 ms |
| T7 | If FSMU in following state cannot transfer to standby mode in 400 ms, it will be restarted |
| T8 | CP cannot stay in pause state more than 400 ms |
FMC: fundamental modeling concepts; FSMU: fail-safe management unit; MP: main processor; CP: communication processor.
Simulation and verification
Simulation
Using the simulator provided by UPPAAL, users can run the FMC model manually and choose which transitions to take, trigger the random mode to let the system run on its own, or go through a trace to see whether certain states are reachable. By this way, we can simulate the behaviors of different components in the FMC model under all kinds of stochastic conditions which is a time-consuming work if implemented manually. In the following subsection, we choose two typical scenarios to illustrate the simulation process.
Scenario 1
In the first example, we choose the function requirements F3 from [Table 3] which is a prerequisite of entering standby mode.
Table 3.
Function properties.
| Req. ID | Function properties |
| F1 | A [] not deadlock |
| F2 | E <> (FSMUA.Host == true & & MPA1.Standby == true) |
| E <> (FSMUB.Host == true & & MPB1.Standby == true) | |
| F3 | E <> (FSMUA.Host == true & & FSMUB.Standby == true) |
| F4 | A [] not (FSMUA.Host == true & & FSMUB.Host == true) |
| A [] not (MPA1.Host == true & & MPB2.Host == true) | |
| F5 | A [] ((FSMUA.Fault == true & & FSMUB.Standby == true) imply (FSMUB.Host == true)) |
| F6 | E <> (FSMUA.H_StateCompare == true & & FSMUB.S_StateCompare == true) |
| F7 | A [] (bPowerA == false imply (MUA.resetNum == 3 & & FSMUA.NoPower == true & & MPA1. NoPower == true)) |
| F8 | A [] not (FSMUA.Start == true & & FSMUB.Start == true & & CP1.Working == true) |
According to the control law of FMC model, working in hot backup mode means that one channel is in host state and the other one is in standby mode. To guarantee the consistence of computation results from host mode channel and backup mode channel, any channel should enter the following mode to study the historical information received from host channel before getting into standby mode. In order to simulate this process, we first set FSMUB, MPB1, and MPB2 to work in host state. Then, let FSMUA, MPA1, and MPA2 power up. As depicted in [Figure 8], before FSMUA, MPA1, and MPA2 are converted to standby mode, they enter the following mode to learn the historical information received from FSMUB, MPB1, and MPB2, respectively. Only if the succuss commands, which declare the study procedure is completed, all the processors in following mode are able to enter standby mode. The results of simulation ensure that the function requirements F3 are logically correct.
Figure 8.
Simulation of following process.
[Image omitted: See PDF.]
Scenario 2
Another example we want to discuss here is function requirements F5. This item details the availability of 2 × 2-out-of-2 safety computer platform which is thought to be one of the most important features of this safety-critical system.
In this scenario, as shown in [Figure 9], FSMUA, MPA1, and MPA2 power up first and enter host state. Having completed the following process successfully, FSMUB, MPB1, and MPB2 begin to work in standby mode. To keep the same pace with the channel in host mode, the standby channel should execute the state synchronization process every cycle. If there is no internal error or outside disruption, both channels of the safety computer platform will remain in normal condition. In order to verify whether the standby channel can turn to host state automatically when the host channel is broken down, we simulate a logic calculation error in FSMUA which resets both MPA1 and MPA2. At this time, it is worth noticing that FSMUB, MPB1, and MPB2 transfer to host mode immediately which is consistent with function requirements F5. Thus, the function requirement F5 is validated.
Figure 9.
Transition from standby mode to host mode.
[Image omitted: See PDF.]
Verification
The purpose of the verification is to find the design defects and check whether certain properties are satisfied. Like the model, the requirement specification and timing restrictions should be expressed in a formally well-defined and machine-readable language. In UPPAAL, the query language which is a simplified version of CTL is adopted to describe the related requirements. It consists of path formulae and state formulae. State formulae describe individual states, whereas path formulae quantify over paths or traces of the model to represent reachability, safety, and liveness.
A state formula is an expression, [Formula Omitted: See PDF], that can be evaluated for a state without looking at the behavior of the model. A state is a deadlock state, if there is no outgoing action transitions either from the state itself or any of its delay successors. For the design of 2 × 2-out-of-2 safety computer platform, deadlock state is totally intolerant. In UPPAAL, the deadlock state formula can be employed with the help of reachability and invariantly path formulae.
Reachability properties check whether there exists a path starting at the initial state, such that [Formula Omitted: See PDF] is eventually satisfied along that path. These properties do not by themselves guarantee the correctness of the safety computer platform, but they validate the basic behavior of the model. Usually, we use the path formula [Formula Omitted: See PDF] to express that some state are satisfied. These properties make sure that every state in safety computer platform is accessible. Safety properties are of the form "something bad will never happen." Let [Formula Omitted: See PDF] be a state formulae. In UPPAAL, we express that [Formula Omitted: See PDF] should be true in all reachable states with the path formulae [Formula Omitted: See PDF], whereas [Formula Omitted: See PDF] says that there should exist a maximal path such that [Formula Omitted: See PDF] is always true. Liveness properties are of the form: "something will eventually happen." Liveness is expressed with the path formula [Formula Omitted: See PDF], meaning [Formula Omitted: See PDF] is eventually satisfied. Another useful form is written [Formula Omitted: See PDF] which is read as whenever [Formula Omitted: See PDF] is satisfied, then eventually [Formula Omitted: See PDF] will be satisfied.
First of all, select a set of requirements from the specification document and transform them into CTL language. Then, take the function and timing properties as the target sets and generate the reachable states set of the FMC model. The UPPAAL verifier can be used to check whether all locations of the model are reachable. The FMC model satisfies the requirements when all executable paths do not contain any dangerous states or forbidden states in short-run future. If not, it is indicated that the model is not correct and needs to be modified. Taking timing property T5 as an example, the verification processes are as follows. In order to verify whether the synchronous tolerance between MPs in the same channel can exceed 20 ms, we should run sequence [Formula Omitted: See PDF] and [Formula Omitted: See PDF], such that (MPA1.Host, MPA1.timer) [Formula Omitted: See PDF] (MPA1.HostSync, MPA1.timer) and (MPA2.Standby, MPA2.timer) [Formula Omitted: See PDF] (MPA2.StandbySync, MPA2.timer), then find out whether | MPA1.timer--MPA2.timer | <20 ms, where {MPA1.Host, MPA1.HostSync, MPA2.Standby, MPA2.StandbySync} [Formula Omitted: See PDF], MPA1.timer and MPA2.timer are clock interpretations.
According to the path formulae of CTL, timing property T5 can be interpreted as follows: (MPA1.HostSync == true & & MPA2.StandbySync == true) imply (| MPA1.timer - MPA2.timer | <20 ms).
It means that synchronous error between MPA1 and MPA2 is usually shorter than 20 ms if the property passes verification. In other words, there should exist a maximal sequence, so that the property T5 is satisfied.
By the same way, we use CTL temporal logic specification language to specify the desired function and timing properties of FMC models. All the properties listed in [Tables 3] and [4] are verified with the help of UPPAAL verifier, assuring that the FMC model can satisfy the function requirements and time characteristics of safety computer platform system.
Table 4.
Timing properties.
| Req. ID | Timing properties |
| T1 | A [] (FSMUA.H_LoopCon imply FSMUA.timer ≤ 400 ms) |
| T2 | A [] not (FSMUA.HostSync == true & & FSMUA.timer > 20 ms) |
| A [] not (FSMUB.StandbySync == true & & FSMUB.timer > 20 ms) | |
| T3 | A [] not (FSMUA.H_CalculateOK == true & & FSMUA.timer > 280 ms) |
| A [] not (FSMUB.S_CalculateOK == true & & FSMUB.timer > 280 ms) | |
| T4 | A [] not (FSMUA.H_OutCompareOK== true & & FSMUA.timer > 320 ms) |
| A [] not (FSMUB.S_OutCompareOK == true & & FSMUB.timer > 320 ms) | |
| T5 | A [] ((MPA1.HostSync == true & & MPA2.StandbySync == true) imply (| MPA1.timer - MPA2.timer | <20 ms)) |
| T6 | A [] not (FSMUA.InitSyn == true & & FSMUA.timer > 400 ms) |
| T7 | A [] ((FSMUA.Following == true and MPA1.timer > 400 ms)) imply (FSMUA.Start == true) |
| T8 | A [] not (CP1.timer > 400 ms & & CP1.Pause == true) |
Application and performance
The formal modeling and verification method presented above is used in the deployment of 2 × 2-out-of-2 safety computer platform. In order to overcome the flaws of anomalous errors, differentiation concept is adopted. MPs run in the same channel, and CPs run in different software versions. One version is designed utilizing conventional method, and the other one is developed with the proposed scheme. First, FMC model is built according to system specifications considering timing constraints and action sets between component automata. Second, function requirements and timing requirements are formalized as CTL properties. Next, all the function properties and timing properties are verified by UPPAAL model checker. Design specifications which do not satisfy some safety properties or timing properties are revised until they meet application requirements. Finally, according to the formal description, the safety computer platform software is refined and implemented using the C language over VxWorks real-time operating system.
Independent developing teams with similar experience and technical level are employed to execute concurrent development. We record the working time in the development of safety computer platform for both teams. It is worth noticing that although it seems time-consuming in modeling and verification procedure, it turns out to be time-saving compared to conventional method if developing and testing time are counted as a whole. As shown in [Figure 10], approximately 9% of the total developing and testing time is saved. Less time consumption does not lead to quality reduction. On the contrary, formal modeling and verification make further improvement on the quality. It is obvious from [Figure 11] that design flaws are reduced nearly 52% in the testing phase, and the total testing time is decreased accordingly. The experimental results indicate that this method consequentially helps us shorten design cycle and enhance quality.
Figure 10.
Developing and testing time analysis.
[Image omitted: See PDF.]
Figure 11.
Errors detected in test phase.
[Image omitted: See PDF.]
Conclusion
With the main goal of allowing engineers and designers to describe safety computer platform system safely and efficiently, this article presents a novel method for modeling and verifying such real-time systems. The 2 × 2-out-of-2 safety computer platform is described in TAN which introduces temporal properties in a simple and explicit manner. FMC model for safety computer platform is built, and the function requirements, real-time properties as well as safety properties are verified using UPPAAL. Simulation and verification results indicate that this provides great assistance for designers to develop more efficient and reliable real-time systems.
Furthermore, this safety computer platform has been applied to Beijing subway line 7, Yizhuang line, and Changping line. It is also expected that the development of other safety-critical systems in automatic train control fields will be significantly accelerated with the help of the proposed method, and the safety will be remarkably enhanced as well.
The authors would like to thank the reviewers for their valuable comments and suggestions.
Academic Editor: Nasim Ullah
Declaration of conflicting interests
The author(s) declared no potential conflicts of interest with respect to the research, authorship, and/or publication of this article.
Funding
The author(s) disclosed receipt of the following financial support for the research, authorship, and/or publication of this article: This paper was sponsored in part by Beijing Laboratory of Urban Rail Transit and Beijing Key Laboratory of Urban Rail Transit Automation and Control, and by Beijing Jiaotong University Technology Funding Project under grant No. W16JB00420.
1, Yan, F, Tang, T, A formal modeling and verification approach for real-time system, In: Proceedings of the 7th world congress on intelligent control and automation, Chongqing, China, 25-27 June 2008, pp.204-208, New York, IEEE.
2, Zhu, L, Yu, FR, Ning, B, Design and performance enhancements in communication-based train control systems with coordinated multipoint transmission and reception, IEEE T Intell Transp, 2014, ; 15, 1258-1272.
3, Sun, WC, Zhao, ZL, Gao, HJ., Saturated adaptive robust control for active suspension systems, IEEE T Ind Electron, 2013, ; 60, 3889-3896.
4, Wan, YB, Xu, ZW, Mei, M., Modeling and formal verification of temporary speed restriction server for CTCS level 3, J Syst Simul, 2013, ; 21, 132-138.
5, Sun, WC, Gao, HJ, Yao, B., Adaptive robust vibration control of full-car active suspensions with electrohydraulic actuators, IEEE T Contr Syst T, 2013, ; 21, 2417-2422.
6, Cheng, RJ, Zhou, J, Chen, DW, Model-based verification method for solving the parameter uncertainty in the train control system, Reliab Eng Syst Safe, 2016, ; 145, 169-182.
7, Wang, X, Tang, T, Study on modeling and verification of CBTC interlocking system, In: Proceedings of the IET international conference on wireless, mobile and multimedia networks, Beijing, China, 22-25 November 2013, pp.350-354, New York, IEEE.
8, Rodriguez-Navas, G, Proenza, J., Using timed automata for modeling distributed systems with clocks: challenges and solutions, IEEE T Software Eng, 2013, ; 39, 857-868.
9, Nemeth, E, Bartha, T., Formal verification of safety functions by reinterpretation of functional block based specifications, IEEE T Software Eng, 2009, ; 39, 857-868.
10, Mokadem, HB, Berard, B, Gourcuff, V, Verification of a timed multitask system with UPPAAL, IEEE T Autom Sci Eng, 2010, ; 7, 921-932.
11, Navimipour, NJ., A formal approach for the specification and verification of a trustworthy human resource discovery mechanism in the expert cloud, Expert Syst Appl, 2015, ; 42, 6112-6131.
12, Henriksson, A, Asman, U, Hunt, J., Improving software quality in safety-critical applications by model-driven verification, Electron Notes Theor Comput Sci, 2005, ; 133, 101-117.
13, Cimatti, A, Giunchiglia, F, Mongardi, G, Formal verification of a railway interlocking system using model checking, Form Asp Comput, 1998, ; 10, 361-380.
14, Zhang, Y, Tang, T, Li, KP, Formal verification of safety protocol in train control system, Sci China Technol Sci, 2011, ; 54, 3078-3090.
15, Ahmad, E, Dong, Y, Larson, B, Behavior modeling and verification of movement authority scenario of Chinese train control system using AADL, Sci China Inform Sci, 2015, ; 58, 1-20.
16, Nicolaidis, M., Fail-safe interfaces for VLSI: theoretical foundations and implementation, IEEE T Comput, 1998, ; 47, 62-77.
17, IEC 61508:2000, Functional safety of electrical/electronic/programmable electronic safety related systems.
18, Ma, LC, Gao, BL., Design and realization of highly safe fault tolerant control computer, China Saf Sci J, 2004, ; 14, 101-105.
19, Chen, SQ, Tang, T, Ma, LC, Design and realization of key algorithms about 2 × 2-out-of-2 vital computer, Comput Secur, 2008, ; 14, 21-23.
20, Sreekumar, A, Swetha, K, Swetha, A, Enhanced performance capability in a dual redundant avionics platform-fault tolerant scheduling with comparative evaluation, Proced Comput Sci, 2015, ; 46, 921-932.
21, Dawkins, S, Kelly, T, Supporting the use of COTS in safety critical applications, In: Proceedings of the IEE colloquium on cots and safety critical systems, 1997, pp.1-8, https://www-users.cs.york.ac.uk/tpk/cots.pdf.
22, Wang, X, Tang, T, A fail-safe infrastructure designed for COTS component used in safety critical system, In: Proceedings of the international conference on signal processing, Beijing, China, 21-25 October 2012, pp.2208-2211, New York, IEEE.
23, Chakraborty, A, Fault tolerant fail safe system for railway signalling, In: Proceedings of the world congress on engineering and computer science, 20-22 October 2009, http://www.iaeng.org/publication/WCECS2009/WCECS2009_pp1177-1183.pdf.
24, Lee, JD, Bhojwani, PS, Mahapatra, RN, A safety analysis framework for COTS microprocessors in safety-critical applications, In: Proceedings of the IEEE high assurance systems engineering symposium, Plano, TX, 14-16 November 2007, pp.407-408, New York, IEEE.
25, Alur, R, Dill, DL., A theory of timed automata, Theor Comput Sci, 1994, ; 126, 183-235.
26, Behrmann, G, David, A, Larsen, KG., A tutorial on UPPAAL, In: Bernardo, M, Corradini, F, (eds) Formal methods for the design of real-time systems, Berlin, Springer, 2004, pp.200-236.
27, Lv, JD, Tang, T, Formal modeling and analysis of RBC subsystem in CTCS level 3 using UPPAAL, In: Proceedings of the WRI world congress, Los Angeles, CA, 31 March-2 April 2009, pp.49-53, New York, IEEE.
© The Author(s) 2016