| Presentation | 2012-12-14 Research on Formalization and Analysis of Automatic Train Protection and Block System Guo Xie, Hiroshi Mochiizuki, Sei Takahashi, Hideo Nakamura, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | A novel train radio system, namely automatic train protection and block (ATPB), is proposed to reconstruct and improve the efficiency of the conventional rail lines. In development of the software system of the ATPB, the formal method is intended to be used to formally analyze its functional requirements specification (FRS) to guarantee the safety and reliability. Firstly, the FRS is written informally in natural language (i.e. Japanese). In order to ensure the correspondence between the natural language specification and the formal specification, a new strategy is proposed, including establishing the dynamic state translations (DSTs), UML diagrams and formal VDM++ model, and verifying the internal consistence of specification. In this paper, only the DSTs are discussed. They expressed the train operation process and the state changes of components, and helped to determine the system parameters. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Railway System / ATPB / Formal Methods / Specification |
| Paper # | DC2012-78 |
| Date of Issue |
| Conference Information | |
| Committee | DC |
|---|---|
| Conference Date | 2012/12/7(1days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | |
| Vice Chair | |
| Secretary | |
| Assistant | |
| Paper Information | |
| Registration To | Dependable Computing (DC) |
|---|---|
| Language | ENG |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Research on Formalization and Analysis of Automatic Train Protection and Block System |
| Sub Title (in English) | |
| Keyword(1) | Railway System |
| Keyword(2) | ATPB |
| Keyword(3) | Formal Methods |
| Keyword(4) | Specification |
| 1st Author's Name | Guo Xie |
| 1st Author's Affiliation | College of Science and Technology Nihon University() |
| 2nd Author's Name | Hiroshi Mochiizuki |
| 2nd Author's Affiliation | College of Science and Technology Nihon University |
| 3rd Author's Name | Sei Takahashi |
| 3rd Author's Affiliation | College of Science and Technology Nihon University |
| 4th Author's Name | Hideo Nakamura |
| 4th Author's Affiliation | College of Science and Technology Nihon University |
| Date | 2012-12-14 |
| Paper # | DC2012-78 |
| Volume (vol) | vol.112 |
| Number (no) | 362 |
| Page | pp.pp.- |
| #Pages | 4 |
| Date of Issue | |