Formal Modelling of the Multiple Trains Following Operation in Uncertain Environments

Ensuring the safety of the following operation under moving block signal is very important for safe operation. Now that the Train Control system under Moving Block Signal (TC-MBS) is a distributed, complex, dynamic, and highly interactive system, the proposed method uses the Multi-Agent System (MAS) technique to design, model, and analyse the TC-MBS system. This paper describes implementing formal methods for modelling the TC-MBS system that operates in an uncertain environment and its safety verification based on model checking techniques. First, the multi-mode following operation in an uncertain environment is analysed using the decision table technique. Second, we introduce a creative modelling approach for MAS called UML-MAS to build the semi-formal model of the TC-MBS system. UML-MAS acts as a standard interface for the system designers and infrastructure managers to increase their requirement comprehension, analysis, system design, and scheme planning at the conceptual level. Thirdly, a set of rules is suggested to convert UML-MAS model into Vector-based Interpreted Systems Programming Language (VISPL) model, which serves as the input for the model checker MCMAS- T. In order to demonstrate the practicality and effectiveness of the suggested approach, some case studies on modelling the TC-MBS systems while considering various scenarios in an uncertain environment and their verification employing MCMAS- Tare presented.