Font Size: a A A

Formal Modeling And Verification Of Safety-critical Communication System

Posted on:2012-01-07Degree:DoctorType:Dissertation
Country:ChinaCandidate:C Z ZhengFull Text:PDF
GTID:1108330377483336Subject:Traffic Information Engineering & Control
Abstract/Summary:PDF Full Text Request
With the deep integration of computer, communication and control technology, and the rapid development of communication technology, communication plays an increasingly important role in safety-critical control areas, such as railway signal, aviation and aerospace etc.. Some of the safety-critical control systems (SCS) require a high level of safety integrity and a mass of safety-related communication (SRC) transmission. The High-speed train control system is one of such systems. In these systems, to separate the safety-related communication out would optimize the system structure, improve the system performance, advance the system development and the safety verification. Such systems, as high-speed railway control system, are safety-critical system with ever more complex hardware integration and software scale, and to use formal method based on rigorous mathematical definition onto them can effectively compensate for the deficiency of traditional performance verification method.The author analyzes the requirements of safety-critical performance and safety-related communication in high-speed railway train control system, then develops a computer-based safety-related information communication system used in level-3 Chinese Train Control System (CTCS-3) ground equipment. From the perspective of safety-critical communication system, the author make use of formal methods into R&D work of computer based communication system in high-speed railway train control system for the first time, and uses repairable Dynamic Fault Tree (RDFT) method to verify the safety of system’s multi-mode redundant structure, uses Colored Petri-net (CPN) method to verify the safety of system’s protocol. Thesis’s works are as follows:1. Thesis summarizes the formal methods used in areas of safety-critical control system; aimed at the design of safety-critical communication system (SCCS) in CTCS-3’s ground equipment, analyzes and selects 2 seemly methods for modeling and verification: RDFTA and CPN methods.2. Aimed at the characteristics of SCCS, thesis analyzes the system’s requirements of safety-critical performance and safety-related communication, implementsa design of SCCS named TSRS safety communication Machine (TSRS-SCM) used in CTCS-3’s ground equipment TSRS, develops a system hardware and software platform, realizes the safety-related communication function.3. Aimed at the TSRS-SCM’s multi-mode redundant security structure, thesis proposes a Repaire Box (RB) based method: repairable DFT (RDFT) modeling and analysis, and puts forward formal semantic of RB; uses the RDFT analysis method to the SCM system structure and related function platform’s modeling & safety analysis; calculates the top event probability of the overall device and verifies system safety.4. Aimed at the TSRS-SCM’s safety-related communication function, thesis use the CPN method to Chinese Railway Signal Safety Protocol RSSP-II protocol’s modeling and verification; analyzes the functions of the Adaptation & redundancy management Layer Entity (ALE) and the Safe Application Intermediate sub-layer (SAI); verifies the protocol’s safety by a mass of simulation conclusion.
Keywords/Search Tags:Safety-critical, Multi-mode Redundant, Safety-related Communication, Repairable Dynamic Fault Tree, Colored Petri-net
PDF Full Text Request
Related items