Presentation | 2010-12-10 Verification of Automatic Block System for Single Line by Model Checking Natsuki TERADA, |
---|---|
PDF Download Page | PDF download Page Link |
Abstract(in Japanese) | (See Japanese page) |
Abstract(in English) | Formal methods is expected to increase reliablity of software. We reported application of B-method to automatic block system for single line. As an different approach from theorem proving, we applied model checking to automatic block system. We described the precise of the verification, then we compare the two different methods. |
Keyword(in Japanese) | (See Japanese page) |
Keyword(in English) | railway signalling / formal methods / model checking / SPIN / automatic block system for single line / B-method |
Paper # | DC2010-57 |
Date of Issue |
Conference Information | |
Committee | DC |
---|---|
Conference Date | 2010/12/3(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 | JPN |
Title (in Japanese) | (See Japanese page) |
Sub Title (in Japanese) | (See Japanese page) |
Title (in English) | Verification of Automatic Block System for Single Line by Model Checking |
Sub Title (in English) | |
Keyword(1) | railway signalling |
Keyword(2) | formal methods |
Keyword(3) | model checking |
Keyword(4) | SPIN |
Keyword(5) | automatic block system for single line |
Keyword(6) | B-method |
1st Author's Name | Natsuki TERADA |
1st Author's Affiliation | Railway Technical Research Institute() |
Date | 2010-12-10 |
Paper # | DC2010-57 |
Volume (vol) | vol.110 |
Number (no) | 333 |
Page | pp.pp.- |
#Pages | 5 |
Date of Issue |