| Presentation | 2012-12-14 Verification of Automatic Block System for Single Line Using SMT Solver Natsuki TERADA, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | Formal methods are expected to increase reliability of software, including that of signaling systems. We modeled the specification of automatic block systems for single line with formal specification languages, and verified the model with SMT (Satisfiability Modulo Theories) solver. SMT solver can easily find truth of the difficult proposition, but the domain of the proposition has some restrictions. We also compare SAT/SMT solver with theorem proving as verification method. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | railway signalling / formal methods / SAT solver / SMT solver / automatic block system for single line |
| Paper # | DC2012-79 |
| 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 | 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 Using SMT Solver |
| Sub Title (in English) | |
| Keyword(1) | railway signalling |
| Keyword(2) | formal methods |
| Keyword(3) | SAT solver |
| Keyword(4) | SMT solver |
| Keyword(5) | automatic block system for single line |
| 1st Author's Name | Natsuki TERADA |
| 1st Author's Affiliation | Railway Technical Research Institute() |
| Date | 2012-12-14 |
| Paper # | DC2012-79 |
| Volume (vol) | vol.112 |
| Number (no) | 362 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |