Keeping the trains and tracks in a safe state is important for railway systems, which include automated control. ATO-2000 is an automated railway system that plans, operates, monitors and controls a small railway network of driver-less trains within a mine. The formal specifications, design and implementation of Checker Function (CF), a software sub-system responsible for maintaining safety in ATO-2000 are described. CF is an important component in a safety-critical, real-time, distributed, mobile computing system. The formal specifications (in Z) of the core safety requirements in ATO-2000 are presented which include a new representation of the track topology. Some fault tolerance of the data received from the field is achieved through data validation constraints. Command safety constraints conservatively validate outgoing commands so that no possible future system state is unsafe. A simple approach used to integrate formal methods in the industrial software development process is discussed. The paper concludes with a review of the lessons learnt.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Safety checking in an automatic train operation system


    Contributors:

    Published in:

    Publication date :

    2001


    Size :

    14 Seiten, 17 Quellen




    Type of media :

    Article (Journal)


    Type of material :

    Print


    Language :

    English




    Automatic test method and device for checking train safety position calculation

    ZHANG XIAOYU / SONG YOUWEI / NIE PENGFEI et al. | European Patent Office | 2023

    Free access

    AUTOMATIC TRAIN OPERATION ASSISTANCE DEVICE, AUTOMATIC TRAIN OPERATION ASSISTANCE SYSTEM, AND AUTOMATIC TRAIN OPERATION ASSISTANCE METHOD

    TACHIBANA HIRONORI / SHIMAYOSHI SHOTA / UEDA KENJI et al. | European Patent Office | 2023

    Free access

    TRAIN AUTOMATIC OPERATION SYSTEM

    YOSHIHARA KENJI / SATO TAKAHIRO / IKEDA HIROYUKI et al. | European Patent Office | 2020

    Free access

    TRAIN AUTOMATIC OPERATION SYSTEM

    YOSHIHARA KENJI / YOKOYAMA HIROYUKI | European Patent Office | 2021

    Free access

    AUTOMATIC TRAIN OPERATION SYSTEM

    HARADA RYOICHI / URA KOSEI | European Patent Office | 2019

    Free access