Due to the harsh environment and rare human presence in the western region, compared with existing train control systems, a new type of train control system(CTCSn) no longer has interval trackside circuits and changes the traditional structure of “ground equipment as the core”. In order to verify the correctness of CTCS-n specifications and verify whether the system meets reliability requirements, this paper proposes a modeling and validation method based on SysML and timed automata(TA). Firstly, the newly added train integrity inspection function in CTCS-n is selected as the research object, and the SysML sequence diagram and activity diagram are used for modeling based on its scene characteristics. According to the conversion rules, the SysML model is converted into the corresponding timed automata network model, which is simulated and verified by using the UPPAAL verification tool. Then the faults of the train integrity function are categorized, and each type of faults is injected into its scenario model to verify its scenario function failure. And the integrity loss fault is injected into the level conversion scenario to verify the impact of the faults on the scenario realization. The results show that the system functional requirements and fault handling meet the system specification requirements.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Formal Verification of Key Function of a New Type of Train Control System Based on Timed Automata


    Beteiligte:
    Li, Aiying (Autor:in) / Liu, Yu (Autor:in) / Yuan, Lei (Autor:in) / Wei, Guodong (Autor:in)


    Erscheinungsdatum :

    24.09.2024


    Format / Umfang :

    1807227 byte





    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    Towards a Digital Highway Code using Formal Modelling and Verification of Timed Automata

    Alves, Gleifer Vaz / Schwammberger, Maike / Luckcuck, Matt et al. | DataCite | 2022

    Freier Zugriff

    Towards a Digital Highway Code using Formal Modelling and Verification of Timed Automata

    Alves, Gleifer Vaz / Schwammberger, Maike | ArXiv | 2022

    Freier Zugriff

    Train Resources Conflict Detection of NGTC Based on Probabilistic Timed Automata

    Gao, Jinjin / Lv, Jidong / Chai, Ming et al. | IEEE | 2021


    Runtime Verification of Railway Interlocking Software with Parametric Timed Automata

    Chai, Ming / Wang, Haifeng / Zhang, Jian et al. | IEEE | 2018


    Runtime Verification of Communications-based Train Control with Parametric Hybrid Automata

    Chai, Ming / Wang, Haifeng / Liu, Hongjie et al. | IEEE | 2019