Research on Development of a Safe and Reliable Software System for Automatic Train Protection and Block System

この論文をさがす

抄録

This paper makes a formal analysis of the specification for a novel railway signaling system, Automatic Train Protection and Block (ATPB) system, which is proposed by the authors to aid in restructuring regional rail lines at low cost in Japan. Firstly, after analyzing the requirements of the ATPB, state transitions for every component are created to express the internal mechanism. Then on the basis of original specification in natural language and state transitions, a rigorous specification of the ATPB is established in VDM++ without ambiguities. Thirdly, in order to guarantee that there are no runtime errors resulting from the internal inconsistency of specification, the internal consistency of VDM++ specification is proved. Followed by the satisfiability is checked by systematic testing to make sure the specification satisfies actual functional requirements. Lastly, the system is simulated strictly according to the formal specification. The simulation met functional requirements well, and illustrated high robustness with internal consistency.

収録刊行物

参考文献 (20)*注記

もっと見る

詳細情報 詳細情報について

問題の指摘

ページトップへ