| Presentation | 2012-05-24 Model Based Specification Validation for a Novel Railway Signalling System Guo Xie, Tomoya Kuroda, Hiroshi Mochizuki, Sei Takahashi, Hideo Nakamura, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | In the development of automatic train protection and block (ATPB) railway signalling system, in order to guarantee the safety and reliability of its software system, formal method is adopted to analyze specification formally. Firstly, in order to improve the accuracy of translating original specification into formal specification, dynamic state translation is extracted to express the internal operation mechanism and state changes for every component, e.g. point, signals, trains. Followed by UML model is created for a comprehensive and object-oriented analysis of ATPB. Thirdly, a rigorous specification of system is established by VDM++ unambiguously without understanding deviation. At last, the specification is validated, such as internal consistency and combinatorial testing to ensure not only the correctness of specification itself, but also the satisfiability for the actual requirement. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Railway Signalling System / ATPB / Formal Methods / Specification |
| Paper # | SSS2012-4 |
| Date of Issue |
| Conference Information | |
| Committee | SSS |
|---|---|
| Conference Date | 2012/5/17(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 | Safety (SSS) |
|---|---|
| Language | ENG |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Model Based Specification Validation for a Novel Railway Signalling System |
| Sub Title (in English) | |
| Keyword(1) | Railway Signalling 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 | Tomoya Kuroda |
| 2nd Author's Affiliation | College of Science and Technology, Nihon University |
| 3rd Author's Name | Hiroshi Mochizuki |
| 3rd Author's Affiliation | College of Science and Technology, Nihon University |
| 4th Author's Name | Sei Takahashi |
| 4th Author's Affiliation | College of Science and Technology, Nihon University |
| 5th Author's Name | Hideo Nakamura |
| 5th Author's Affiliation | College of Science and Technology, Nihon University |
| Date | 2012-05-24 |
| Paper # | SSS2012-4 |
| Volume (vol) | vol.112 |
| Number (no) | 52 |
| Page | pp.pp.- |
| #Pages | 4 |
| Date of Issue | |