Dealing with the ever-growing complexity of railway systems requires scalable approaches for detecting inconsistent safety requirements in practice. Despite significant efforts to automate the requirements consistency detection, current inconsistency analysis techniques of railway safety requirements still suffer from scalability issues. This paper proposes a two-layer approach for detecting inconsistencies in time-related safety requirements of railway systems, integrating two distinct formal methods from a pragmatic perspective. At the SafeNL layer, we employ an SMT-based approach to extract conflict patterns and use them to filter out inconsistent requirements descriptions, thus avoiding the more expensive general use of the SMT-based approach. At the CCSL layer, temporal dependencies in requirements are transformed into causal relations, which are then detected for circular inconsistencies using a graph search technique. Our evaluations demonstrate the utility and scalability of our approach.

Consistency verification of safety requirements is crucial for the success of safety-critical systems, particularly railway systems. However, this task often requires significant time spent on interaction and communication between domain experts, who possess in-depth knowledge of safety requirements in a specific domain, and formal experts, who have the necessary skills to apply verification tools and techniques. To enhance time efficiency and productivity, we propose an approach to empower domain experts with formal methods for verifying safety requirements’ consistency. This involves transforming natural requirements into formal models and using formal methods for verification. The approach also localizes inconsistent requirements to provide feedback to domain experts. Communication between domain experts and formal experts can be facilitated through the pattern language SafeNL. By adopting this approach, domain experts can utilize formal verification without extensive consultation with formal experts. Two practical case studies with CASCO Signal Ltd. validate its effectiveness, practicality, as well as a significant reduction of time compared to traditional methods (at least 90% reduction). This reduction in time is primarily due to reduced communication needs and more efficient localization. Evaluations show that SafeNL is user-friendly and the approach performs well in modular systems while scalability is somewhat limited.

Although there has been substantial research in system analytics for risk assessment in traditional methods, little work has been done for safety risk prediction in communication-based train control (CBTC) system, especially intelligently predicting risk caused by the uncertainty in the system operation. Risk prediction and assessment of hazards in train control systems are vital for the safety and efficiency of urban rail transit. In this paper, we propose an intelligent hazard-risk prediction model based on a deep recurrent neural network for a new communication-mode CBTC system. First, a train-to-train communication-based train control (T2T-CBTC) system is proposed to improve the drawback of CBTC in information-exchanging mode. Then we design a risk prediction feature selection and generation method and estimate a critical function feature in the T2T-CBTC system by statistical model checking. Finally, we construct our intelligent hazard-risk prediction model based on a deep recurrent neural network using a long-short-term memory (LSTM) network. The model had excellent risk prediction classification results and performance in our experiment, even for unbalanced data set. This model consistently outperforms the deep belief network trained in Accuracy, Precision, Recall and F1-score for the hazard-risk prediction problem. Specifically, the mean accuracy is 97.2% and mean F1-score is 93.9% in overall performance of model. The improvements of our model against DBN model are 8.2% for Precision, 7% for Recall and 8% for F1-score.

Consistency verification of safety requirements is an important but still challenging task for safety-critical systems such as rail transit systems. That is mainly because requirements are typically written in natural language and with strong time constraints. Driven by the practical need from industry, in this paper we propose a systematic approach to specify safety requirements in a quasi-natural language and automatically verify their consistency using formal methods. Specifically, we define a domain specific language SafeNL to specify safety requirements, and then automatically transform them into formal constraints defined in the Clock Constraint Specification Language (CCSL). The transformed constraints can be automatically and efficiently verified by model checking. We conduct two practical case studies to analyze the safety requirements of an interlocking system in CASCO Signal Ltd. Results of the studies show the validity and utility of our approach can pragmatically contribute to industrial practice. We also report some lessons learned from case studies.

Formal methods have been applied widely to verifying the safety requirements of communication-based train control (CBTC) systems, while the problem situations could be much simplified. In industrial practices of CBTC systems, however, huge complexity arises, which renders those methods nearly impossible to apply. In this paper, we aim to reduce the state space of formal verification problems in zone controller, a sub-system of a typical CBTC. We achieve the simplification goal by reducing the total number of device variables. To do this, two projection methods are proposed based on problem frames and constraints, respectively. The problem frame-based method decomposes the system according to sub-properties through functional decomposition, while the constraint-based projection method removes redundant variables. Our industrial case study demonstrates the feasibility through an evaluation, confirming that these two methods are effective in reducing the state spaces of complex verification problems in this application domain.

The safety prediction of rail transit system is a fundamental problem in rail transit modeling and management. In this paper, we propose a safety prediction model based on deep learning for rail transit safety, which has been implemented as a deep belief network (DBN). It can learn effective features for rail transit prediction in an unsupervised fashion, which has been examined and found to be effective for many areas such as image and audio classification. To increase the accuracy of prediction, we introduce user satisfaction and rare-event probability, the new input prediction factors, into safety prediction. The former takes account of human and the latter is computed by statistic model checking. To show proof of the model, a real-world subway data sets based on the Beijing Metro in China is presented to demonstrate the feasibility of the model. Experiments on data sets show good performance of our prediction. These positive results demonstrate that deep learning and new factors are promising in rail transit research.

Interlocking system is an important module to ensure traffic safety. However it is still very difficult to apply automatic testing in industrial application. In this paper, we propose an approach to generate test case automatically with the help of SMT Solver. First, we extract the yard specification written by boolean expressions from interlocking rules and configuration specification. And then a process to generate test cases based on the specification is given. Finally, We apply our approach to the interlocking system at LongXiLu station in China.

The hybrid architecture analysis and design language (AADL) has been proposed to model the interactions between embedded control systems and continuous physical environment. However, the worst-case performance analysis of hybrid AADL designs often leads to overly pessimistic estimations, and is not suitable for accurate reasoning about overall system performance, in particular when the system closely interacts with an uncertain external environment. To address this challenge, this paper proposes a statistical model checking-based framework that can perform quantitative evaluation of uncertainty-aware hybrid AADL designs against various performance queries. Our approach extends hybrid AADL to support the modeling of environment uncertainties. Furthermore, we propose a set of transformation rules that can automatically translate AADL designs together with designers' requirements into networks of priced timed automata and performance queries, respectively. Comprehensive experimental results on the movement authority scenario of Chinese train control system level 3 demonstrate the effectiveness of our approach.

The integration of formal methods and requirements analysis increases the dependability of safety-critical systems. However it is still very difficult to obtain all of the safety requirements in practice, and formally construct the safety requirements model as well. In this paper, we propose an approach to capture safety requirements and formally describe them by classifying and developing safety requirements specification patterns. Our classification is a result of extracting safety properties from a variety of sources, such as interlocking tables and existing safety relevant functional requirements of railway interlocking system. They contain safety properties at analysis level and design level respectively. Furthermore, safety specification patterns based on the classification are used to formally describe and organize the safety requirements for formal verification. Finally, a tool called SRSV has been developed to enhance the process from deriving safety requirements to verifying. We applied it to the interlocking system at Mohe station in China, and the generated safety properties were then checked to hold by the verification tool.

In recent years, with gradual application of formal verification methods to automatic train control (ATC) systems, the problem of verification failure occurs due to the complexity of the verification system. In order to solve this problem, this paper proposes a safety attribute based projection for the ATC systems. We describe this verification system using Problem Frames approach and define projection operators. By projection, the original verification system is divided into several sub-systems. An experiment is also conducted with data collected from a metro line. The experimental results show that the projection can effectively simplify the system state, and increase the efficiency of formal verification.

Automation and high coverage are two essential industrial technical requirements of qualified testing method for safety-critical systems. The ioco-testing method is a sound and well-defined formal automation testing technique for labelled transition system. However, when we apply this method to a train control system developed by our industrial partner, we find that some testing requirements are not covered for certain testing objects. Further analysis has shown that the ioco-testing method only generates test cases based on explicit specified system behaviors which may result in low coverage when the implementation under test includes code branches used to deal with faults which can't be defined thoroughly in the specification in practices. Therefore, we propose a labelled transition system testing method based on specification mutation to improve safety-critical system testing coverage. We firstly define the mutation operators for the Input output symbolic transition system (IOSTS) modeling language, then we construct the corresponding test generation algorithm and translate the derived test cases into xml files which can be directly applied to the implementation under test in a simulation and test platform developed by our partner. Preliminary experiments on a safety-critical function named train position determination have shown about 28.5% improvement on the testing coverage.