3 / 2018-01-15 19:02:37

Modeling and Verification of Railway Level Crossing Man-agement System Based on Formal Method

railway transportation; railway level crossing; management specifications; formal methods; system prototype; model verification

The accidents of railway crossing account for a large proportion of railway accidents, enhancing the safety of the railway crossing can effectively reduce casualties and property damage and improve the efficiency of the train operation. Based on the man-agement standards of the railway crossings, the requirements of the attributes and the processes of the events were obtained, a multilayer formal model using the Event-B language and refinement policy was established. Through the theorem proving process, the system features of safety and time were proved and the prototype of the system was fixed. Finally, the defects of management specifications were detected, the robustness of the system was increased as well as the correctness of the model was validated by the checking the invariant violations and deadlock. The formal modeling and verification method can be used to check the re-quirement specification of the railway crossing system and form a reliable prototype which deeply improve the safety of the railway crossing.