Z Formal Specification of CBTC Moving Block Interlocking System
Creators
- 1. Acharya Institute of Technology, Visvesvaraya Technological University, INDIA
- 2. P.E.S College of Engineering, Visvesvaraya Technological University, INDIA
Contributors
Contact person:
- 1. Acharya Institute of Technology, Visvesvaraya Technological University, INDIA
Description
Urban railway interlocking system is a safety-critical system, for which interlocking rules are well-defined by international standards to assure safe operations. Nowadays, the Communications-Based Train Control (CBTC) signaling system is adopted in Urban Railway Interlocking System. It broadcast the signals among the trains and trackside objects for traffic management and train control. It also finds more accurately the precise location of the train. Which results in an efficient and safe way to manage the railway traffic flow and reduce the headway between trains.
Z is one of the widely used formal specification methods, that is used to expose requirements problems. To precisely specify both the early and late requirements of a CBTC-based Urban railway interlocking system and verify safety properties, we developed a Z formal model. Here, we presented a Z formal specification of an Urban Railway Interlocking System, which makes use of CBTC as a signal and controlling system. We designed this formal model by translating the iStar goal model of the Urban Railway Interlocking System. This project is a part of my Ph.D. work.
LICENSE
***************************************************************************************
Synopsis [Z Formal Specification of CBTC Moving-Block Interlocking System]
Author [Lokanna Kadakolmath]
Copyright [Copyright (C) 2022, 2023 by Lokanna Kadakolmath and Umesh D. R.
This formal specification is free software: you can redistribute it and/or modify it under the terms of the GNU Affero General Public License as published by the Free Software Foundation, AGPL-3.0-or-later.
This formal specification is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Affero General Public License for more details.
You should have received a copy of the GNU Affero General Public License along with this formal specification. If not, see <https://www.gnu.org/licenses/>.
For more information email to <lokanna@acharya.ac.in> or <lokanna.kadakolmath@gmail.com>]
***************************************************************************************