Data of the train communication network(TCN) is becoming more complicated, which results in higher requirements of the data processing unit-the multifunction vehicle bus controller (MVBC) connected within the TCN. Developing an MVBC is challenging because of the integrated hardware-software solutions to support reactions in real time and dynamic environment. Hence, there is an urgent need for a rigorous design framework to facilitate the development of MVBC. In this paper, we propose a design framework TooMVBC to generate executable MVBC code from formal verified computation model. TooMVBC uses formal computation model MVBChart to capture the specification of the MVBC at high level. First, primitive syntax of MVBChart is designed to model MVBC features (e.g. hierarchy structure, data flow of the encoder, the control logic of communication protocol), and semantics of MVBChart is formalized for simulation and verification. Then, semantics-preserving code generation algorithms are designed to generate VHDL code for partitioned hardware implementations and C code for partitioned software implementations from verified MVBChart model. The generated code can be loaded into the proposed flexible MVBC hardware architecture directly. Finally, supporting graphical model editor, simulator, verification translator, partitioning and code generator are implemented and seamlessly integrated into TooMVBC. When we apply TooMVBC to design MVBC with the highest class 5 according to the description of the standard IEC 61375, several critical ambiguousness or bugs in the standard are detected during formal verification of the constructed system model.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Formal Design of Multi-Function Vehicle Bus Controller


    Contributors:
    Jiang, Yu (author) / Wang, Mingzhe (author) / Su, Zhuo (author) / Yang, Yixiao (author) / Wang, Huihui (author)


    Publication date :

    2021-06-01


    Size :

    1309667 byte




    Type of media :

    Article (Journal)


    Type of material :

    Electronic Resource


    Language :

    English



    Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller

    Jiang, Yu / Liu, Han / Song, Houbing et al. | British Library Conference Proceedings | 2016


    Formal design and analysis of FMS controller

    Xu Gang, / ZhiMing Wu, | IEEE | 2003


    Formal Design and Analysis of FMS Controller

    Xu, G. / Wu, Z. / IEEE | British Library Conference Proceedings | 2003


    Multi-adaptor vehicle remote function controller and associated methods

    FLICK KENNETH E | European Patent Office | 2018

    Free access

    MULTI-ADAPTOR VEHICLE REMOTE FUNCTION CONTROLLER AND ASSOCIATED METHODS

    FLICK KENNETH E | European Patent Office | 2018

    Free access