Research on Development of a Safe and Reliable Software System for Automatic Train Protection and Block System
-
- NAKAMURA Hideo
- College of Science and Technology, Nihon University
Search this article
Abstract
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.
Journal
-
- The Journal of Reliability Engineering Association of Japan
-
The Journal of Reliability Engineering Association of Japan 35 (1), 59-70, 2013
Reliability Engineering Association of Japan
- Tweet
Keywords
Details 詳細情報について
-
- CRID
- 1390001204452353024
-
- NII Article ID
- 110009579103
-
- NII Book ID
- AN10540883
-
- ISSN
- 24242543
- 09192697
-
- NDL BIB ID
- 024242833
-
- Text Lang
- en
-
- Data Source
-
- JaLC
- NDL
- CiNii Articles
-
- Abstract License Flag
- Disallowed