Dissertation > Excellent graduate degree dissertation topics show

Formal Verification of Safety Computer Platform in CBTC System Based on Timed Automata Model

Author: GuoZhiLiang
Tutor: ZuoChunHai
School: Beijing Jiaotong University
Course: Traffic Information Engineering \u0026 Control
Keywords: real-time system safety computer timed automata model verification UPPAAL
CLC: U284.48
Type: Master's thesis
Year: 2010
Downloads: 87
Quote: 1
Read: Download Dissertation

Abstract


In many industrial fields, the running foundation of the computer control system must be highly reliable, highly available and highly safe. Safety computer systems are commonly used in military, aerospace, industrial control, banking, telecommunications and other Safety-Critical areas in order to avoid a major accident caused by a computer failure.CBTC(Communications-Based Train Control) system is the development trend of the world’s train operation control system, and the major developed countries have developed their own CBTC system. In the CBTC system, ZC (Zone Controller) and DSU (Data Storage Unit) are the main components of the ground-based regional control center. All the VOBC (Vehicle On-Board Controller) of the train in the domain of ZC sent the train location and speed to the ZC application program which runs in the safety computer. After the safety calculation, MA (Movement Authorization) is sent to the VOBC to control the train to run next step. And the DSU subsystem includes all the data and configuration files of the other train control subsystem. Moreover, its application software also needs to run on the platform of safety computer.Using the 2×2-out-of-2 redundant structure safety computer platform is an important solution to improve the system’s security and reliability. The safety computer platform of the CBTC trains control system uses the 2×2-out-of-2 structure, and it’s a real-time system taking the time factor into account in the control process. The structure of the safety computer system is analyzed and the function of the system is extracted. The timed automata network model of the system is built using the validation tool UPPAAL based on the theory of timed automata. Then the simulation is carried out, and the function, real-time and safety properties of the system is validated.

Related Dissertations

  1. Research on Detecting the Locomotive Drivers’ Fatigue Based on Computer Vision,TP274
  2. Research on Security of E-Commerce Protocols Based on UPPAAL,TP393.08
  3. The Research on Model Transformation Based on MDE for Real-Time System Verification,TP311.52
  4. Research on Global FP Scheduling Algorithm on Multiprocessor Platform,TP332
  5. Flexible workflow process model,TP311.52
  6. IF graphical models of real-time software design verification,TP311.52
  7. XML-based information conversion and editing systems design,TP311.52
  8. Research on Page Coloring Based Cache Sharing Policies in Multicore RT System,TP332
  9. Improvement Research of Scheduling Analysis Tool for Distributed Real-Time System,TP311.52
  10. Modeling and Verification of On-Board Equipment of CTCS-3 Train Operation Control System Based on Timed Automata,U284.48
  11. Research and Simulation on the Main Function of Vital Computer of CTCS-2 Train Control System,U284.48
  12. Research on Verification of Web Service Composition Based on XYZ/ADL,TP393.09
  13. Embedded systems based on Petri net modeling and validation studies,TP368.1
  14. Verification and Physical Implementaion of G.729 Speech Codec,TN912.32
  15. Realization of ADBF and Adaptive Antenna Side-lobe Cancellation in External Illuminators Based Radar System,TN958.97
  16. Design and implementation of high concurrent performance monitoring system based on the real-time visualization of data mining,TP274
  17. dSPACE applications in process control,TP273
  18. Design and Achievement of a Tool of Modeling, Simulation and Verification of Context Aware System Based on UPPAAL,TP311.52
  19. Schedulability Analysis of Multi-Processor Real-Time Systems Using Uppaal,TP316.2
  20. Modeling and Scheduling Embedded Real-Time System SMILE,TP368.1

CLC: > Transportation > Rail transport > Railway communication,signal > Railway signal > Section block and cab signal system > Train operation automation
© 2012 www.DissertationTopic.Net  Mobile