Loading...
Please wait, while we are loading the content...
Similar Documents
Formal Analysis of Automatic Train Protection and Block System for Regional Line Using VDM
| Content Provider | Semantic Scholar |
|---|---|
| Author | Hei, Xinhong Mochizuki, Hiroshi Takahashi, Sei Nakamura, Hideo |
| Copyright Year | 2012 |
| Abstract | This paper introduced a novel railway system, Automatic Train Protection and Block (ATPB) briefly, which is proposed to improve the efficiency of existing regional train lines with low cost in Japan. The biggest superiority of ATPB system is a great use of universal and mature technologies, such as GPS and regular mobile telephone networks, so that there is nearly no increment of trackside equipments in the reconstruction. Then in order to guarantee the system safety, a formal model of ATPB is established and analyzed by formal method VDM++. Firstly, the specification is specified by VDM++ formally without ambiguity. Secondly, its internal consistency is proved by discharging the proof obligations. And finally, its satisfiability is checked by systematic testing, which executes specification and checks the outputs against corresponding inputs. |
| Starting Page | 65 |
| Ending Page | 70 |
| Page Count | 6 |
| File Format | PDF HTM / HTML |
| DOI | 10.7782/IJR.2012.5.2.065 |
| Volume Number | 5 |
| Alternate Webpage(s) | http://www.ijr.or.kr/On_line/admin/files/(065-070)-12-008.pdf |
| Alternate Webpage(s) | http://ocean.kisti.re.kr/downfile/volume/railway/E1ROBC/2012/v5n2/E1ROBC_2012_v5n2_65.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
