The Research On The Formal Methods Of The Station Interlock Control Logic Based On Event-B And MAS

With the rapid development of China's railway, the concepts of safe and high speed have been regarded as the core standard of railway system.Based on European Train Control system(ETCS), Chinese train control system has been developed with independent property right. The computer interlocking system is the basic facility using the interlocking software under the rapid development of China's railway industry according to “Bug-Safety” principle. The interlocking of station directly relates to the driving safety, and also influences the efficiency of station operation and the traffic organization work. Described in non-formal language and natural semantics, most traditional development of interlocking software mainly applies to the demand-analysis method in software engineering, and are unable to satisfy the security requirements of computer interlocking system in designing, analyzing and testing. To standardize and describe the interlocking system using formal methods not only can improves the quality of computer interlocking software, but also helps to conduct the stricter test.Computer interlocking is the system composed of micro-manipulator software, hardware, electron and electric relays. Computer interlocking system needs a high reliability and safety control system. The significance of interlocking is that the process of route control should be described strictly. Through combining the description of the 6502 electric relay's function to illustrating the station route interlocking control logic, the rigorous mathematical model is used to specify and verify the interlocking system in the formal ways.This thesis is written based on the research of the railway interlocking technology. First of all, focusing on the two formalized methods of Event-B and MAS in the situation of station access, the features and advantages of the two methods are stated in the thesis, and a model to test the safety requirements for control functions of the interlocking technology is built up, using the development platform of Event-B, the Rodin. The interlocking logic relations of railway station access are described in detail, such as the process of signals, turnouts, track sections and annunciations in station access. The features and names of these elements are seen as static information, and their changing states are seen as dynamic information, which are stored in computer storage for generating test result. With the analysis of the result, we can ensure the consistency and integrity, and improve the operation performance and safety of the system software. Then, the thesis introduces the concept of MAS and describes the model of interlocking in framework with MAS, and builds different scenarios of the agents. Finally, the MAS system is formed. The thesis achieves the modeling process in a formal language and generates the proof obligations. The result shows the combined method of formal Event-B and MAS leads to an effectively standardization on the complex logical relations of the model of station interlock routing scene. It not only has a certain reference value to the development of formal methods, but also provides a practical and effective method for the railway interlocking control modeling.