The on-board equipment of Chinese Train Control System-3 (CTCS-3) plays a key role in protecting trains from over-speeding. Conventional over-speed protection methods monitor the speed at discrete time instants. However, behavior between instants cannot be detected, which may cause potential risks. To address this problem, paper proposes hybrid safety observation method to train throughout operation. In proposed method, is modeled with automata, takes parameters that affect movement into...

An innovative topology-based method for modeling railway train control systems is proposed in this paper. The addresses the problems of having to rely too much on designers' experience and incurring excessive cost validation verification development systems. Four topics are discussed paper: 1) definition basic topological units networks, based essential characteristics these units; 2) concept a movement authority space; 3) interpretation logic as space construct; 4) theorems system...

Natural language in the maintenance data of high speed railway system is big challenge for fault diagnosis due to its unstructual feature and uncertainty semantics. In this paper, a text mining based method vehicle on-board equipment (VOBE) has been proposed, which, topic model used extract from records with arbitrary nature. addition, Bayesian network (BN) also adapt complexity VOBE. Furthermore, that fully utilizes domain expert knowledge presented derive an appropriate BN structure At...

A point machine’s gap is an important indication of its healthy status. An edge detection algorithm proposed to measure and calculate a from the image captured by CCD plane arrays. This integrates adaptive wavelet-based denoising, locally binarization, mathematical morphology technologies. The denoising obtains not only optimal threshold, but also unblurred edges. Locally binarization has advantage overcoming local intensity variation in images. Mathematical may suppress speckle spots caused...

Sophisticated hardware/software and harsh environment in safety-critical discrete event systems may cause system failures that can lead to catastrophic consequences. Therefore, keeping the a safe mode even after occurrence of fault is critically important. This paper addresses problem by first extending net condition/event with uncontrollable transitions allows one well represent controllable events cater for modeling normal abnormal systems. A binary decision diagram-based symbolic...

Communication based train control (CBTC) system was on mobile communication and overcome fixed blocks in order to increase track utilization safety. As an intelligent autonomous decentralized systems (IADS), data (DCS) between trains zone center (ZC) are crucial factors for the safe efficient operation of CBTC system. The real-time behavior under various transmission conditions needs be modeled evaluated. paper presents a DCS model evaluates influence collision message length transfer delay....

Interlocking tables, as the function specification of Computer Based System (CBI), play an important role in ensuring safe train movements at a railway station. The development and verification interlocking tables is entirely manual process currently, which inefficient error-prone due to complexity CBI human interferences. In order tackle these problems, we introduce toolset based on Domain Specific Language for Systems (DSL-CBI) automatically generate verify table. this paper, address how...

Communication Based Train Control (CBTC) system is the most advanced train control in world nowadays. How to model and simulate find design defects research development has became one of key issues CBTC research. This paper describes a method developing hierarchy refined modular Vehicle-on-board Automatic Protection (V-ATP) subsystem using Colored Petri Net (CPN). The aim provide simulation environment for V-ATP subsystem.

Risk-based maintenance (RBM) aims to improve planning and decision making by reducing the probability consequences of failure equipment. A new predictive strategy that integrates dynamic evolution model risk assessment is proposed which can be used calculate optimal time with minimal cost safety constraints. The provides qualified risks using probabilistic inference bucket elimination gives prospective degradation trend a complex system. Based on trend, an determined minimizing expected per...

Due to the complexity and size of railway interlocking systems, conventional verification testing techniques are not able provide sufficient safety assurance. This paper proposes an online observer for assurance systems. The provides runtime checking states behaviors devices by using a topology-based mathematical model. Route signals, points, track sections interpreted in topological space, properties expressed as topology theorems. Running synchronously with task, conducts checks on route...

The complexity of software in safety critical systems has increased significantly over the last ten years so that how to tackle and gain high dependable plays an important roles ensuring overall product quality. In this context, component based development (CBD) been successfully applied large scale system fields Software Engineering. Similarly, System Safety Analysis (SSA) also gained wide used But they often their methodology isolation. Furthermore, shortage unified formal framework bridge...

Chinese Train Control System Level 3(CTCS-3) is a typical complex cyber-physical system. The complexity of functionality CTCS-3 brings some challenges to the safety analysis with methods. In this paper, we propose method functional based on hybrid automata, where faults are modeled as fault events present situation system, moreover, transition from automata PHAVer model and monitor which can malfunction in reachability elaborated. At last, take speed supervision an example, experimental...

The RBC (Radio Block Center) handover is an important part of European Train Control System level 2 which a typical safety-critical hybrid system. In this paper, we build formal model procedure using Differential Dynamic Logic, first-order dynamic logic for specifying and verifying systems, identify some constraints that are necessary ensuring safety train control, including collision avoidance as well derailment avoidance. Moreover, formally verify the safety-related properties our with...

As the computer systems become more and complex, project exploitation is difficulty. Unfortunately, many complex system projects are unsuccessful. One of most important reasons lacking requirement management. Therefore, this paper proposes a management approach which based on tool-RequisitePro. The category guiding principle shown, consistency traceability between categories UML model established. In addition, detail train control typical will be shown. result proves that can cover all...

The Chinese train control system level 3 (CTCS-3) requirement specification required to be high-quality should satisfy the quality attributes, such as correctness, completeness, consistency, and traceability. In order prove that these attributes are satisfied, we present a scenario-based approach using UML sequence diagram model checking modeling verify specification. mapping between scenario ensures correctness of modeling, enhances traceability verification. expressiveness precise...

Runtime verification is a promising method that tries to bridge the gap between formal methods and traditional testing. In this paper, we present an improved runtime via multi-valued formula rewriting. A 3-valued executable semantics for finite trace LTL formally defined, algorithm based on new proposed implemented in Maude, which high performance rewriting system. To improve efficiency of our algorithm, introduce novel approximation technique, reduces steps by sacrificing some abilities...

The high quality System Requirement Specification (SRS) is at the heart of design and development European Train Control level 2 (ETCS L2) with safety efficiency.However, SRS, written in natural language a shortage rigorous mathematic foundation, makes it difficult to meet attributes such as correctness, completeness consistency.In order tackle above problems, integration scenariobased model formal method, which recommended verify critical system (e.g., train control system), proposed...

Safety arguments are key components in a safety case. Too often, constructed without proper reasoning., Inappropriate reasoning system's argument could undermine the claims, which turn contributes to safety-related failure of system. To address this, we argue that informal logic schemes have important roles play construction process. Several computer system domain proposed against engineering literature. It is anticipated this work will contribute toward development arguments.

This In this paper a stochastic automation networks (SANs) model for the computing availability of Communication Based Train Control (CBTC) system is developed, which captures lossy radio communication link and transmission procedures based on 802.11 protocols. A scaled generalized minimum residual (SGMRES) iterative method provided to reduce ill-condition steady-state equation state-space explosion problem. The (Mean Time Between Stop, MTBTS) CBTC quantitatively evaluated compared under...

When verifying the safety of ETCS, testing and formal methods have limitations to some degree. Runtime verification is effective detect deviation between current expected system behaviors. To improve accuracy runtime monitoring, 4-valued LTL (Linear Time Logic) semantics formula rewriting based algorithm are proposed. Furthermore, approximation technique presented for formulae make procedure high efficient. Finally, method applied European Train Control System (ETCS) by monitoring several...

Although formal methods (FMs) are highly recommended by several International Standards for safety critical systems, almost all of the existing work on FMs focused models which only have internal inconsistencies. How to guarantee external consistency (or correctness) a model, i.e., satisfying expectations users, is great challenge. In this paper, strategy improve correctness proposed establishing, validating and verifying function model data structure separately, fusing them finally, as...