English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Communication Based Train Control (CBTC) system is the state-of-the-art traincontrol system. In a CBTC system, to guarantee the safety of train operation,trains communicate with each other intensively and adjust their control modesautonomously by computing critical control parameters, e.g. velocity range,according to the information they get. As the correctness of the controlparameters generated are critical to the safety of the system, a method toverify these parameters is a strong desire in the area of train control system.In this paper, we present our ideas of how to model and verify the controlparameter calculations in a CBTC system efficiently. - As the behavior of thesystem is highly nondeterministic, it is difficult to build and verify thecomplete behavior space model of the system online in advance. Thus, we proposeto model the system according to the ongoing behavior model induced by thecontrol parameters. - As the parameters are generated online and updated veryquickly, the verification result will be meaningless if it is given beyond thetime bound, since by that time the model will be changed already. Thus, wepropose a method to verify the existence of certain dangerous scenarios in themodel online quickly. To demonstrate the feasibility of these proposedapproaches, we present the composed linear hybrid automata with readable sharedvariables as a modeling language to model the control parameters calculationand give a path-oriented reachability analysis technique for the scenario-basedverification of this model. We demonstrate the model built for the CBTC system,and show the performance of our technique in fast online verification. Last butnot least, as CBTC system is a typical CPS system, we also give a shortdiscussion of the potential directions for CPS verification in this paper.

Online Verification of Control Parameter Calculations in Communication Based Train Control System