NDLI: Study on Formal Specification of Automatic Train Protection and Block System for Local Line

Content Provider	IEEE Xplore Digital Library
Author	Guo Xie Asano, A. Takahashi, S. Nakamura, H.
Copyright Year	2011
Abstract	This paper presents a formal specification of an Automatic Train Protection and Block (ATPB) model for local line railway system in Japan proposed by the author [12], and validates the model by internal consistency proving and systematic testing. The system consists of two parts, the on-board subsystem and ground subsystem. The former is to detect the basic state of train, such as position, speed and integrity, monitor the speed, communicate with ground equipment and record the relative events. And the latter is responsible for communicating with train, controlling the route and interlocking, and decision-making for train operation adjustment. The main purpose of this project is to improve the efficiency and guarantee that there is no collision, no derailment and no over speeding at the same. The formal language used in this project is VDM++. And the state and specification of operation are all checked and validated using VDMTools. The results confirm the correctness of this system and the model throws new light on practical system design.
Starting Page	35
Ending Page	40
File Size	464961
Page Count	6
File Format	PDF
ISBN	9781457707810
DOI	10.1109/SSIRI-C.2011.16
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2011-06-27
Publisher Place	Korea (South)
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Ground subsystem VDM++ Formal specifications Global Positioning System Systematics Databases VDMTools Railway system Rail transportation Safety ATPB Formal methods On-board subsystem Testing
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Model based specification validation for automatic train protection and block system

Formal Analysis of Automatic Train Protection and Block System for Regional Line Using VDM + +

Research on modeling and simulation of vehicle-on-board Automatic Train Protection subsystem of Communication Based Train Control system

Modeling and Formal Specification of Automated Train Control System using Z Notation

An Automated Approach to Inheritance and Polymorphic Testing using a VDM++ Specification

Formal requirements specification in safety-critical railway signaling system

Formal Analysis of Automatic Train Protection and Block System for Regional Line Using VDM

An automatic SPIN validation of a safety critical railway control system

Formal verification of Communication based Train Control system

Study on Formal Specification of Automatic Train Protection and Block System for Local Line

Similar Documents

Model based specification validation for automatic train protection and block system

Formal Analysis of Automatic Train Protection and Block System for Regional Line Using VDM + +

Research on modeling and simulation of vehicle-on-board Automatic Train Protection subsystem of Communication Based Train Control system

Modeling and Formal Specification of Automated Train Control System using Z Notation

An Automated Approach to Inheritance and Polymorphic Testing using a VDM++ Specification

Formal requirements specification in safety-critical railway signaling system

Formal Analysis of Automatic Train Protection and Block System for Regional Line Using VDM

An automatic SPIN validation of a safety critical railway control system

Formal verification of Communication based Train Control system

Study on Formal Specification of Automatic Train Protection and Block System for Local Line