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