Specification of Train Control Systems Using Formal Methods

摘要

Just as what the public pursue, we need a much safer railway system with a higher level of automation in control. To achieve this goal, the author aims to specify the Train Control System by formal methods which can specify the communication of various processes in the system clearly. This paper applies Timed-CSP which concerns the time-delay to the specification of the control flow and communication among flows in Train Control System, and specifies the state and data change by Object-Z. By Timed-CSP and Object-Z, the specification of a simplified Train Control System especially the time constraints is more concrete.