Safety-assured model-driven design of the multifunction vehicle bus controller

Yu Jiang, Han Liu, Houbing Song, Hui Kong, Rui Wang, Yong Guan, Lui Sha

Research output: Contribution to journalArticlepeer-review


In this paper, we present a formal model-driven design approach to establish a safety-assured implementation of multifunction vehicle bus controller (MVBC), which controls the data transmission among the devices of the vehicle. First, the generic models and safety requirements described in International Electrotechnical Commission Standard 61375 are formalized as time automata and timed computation tree logic formulas, respectively. With model checking tool Uppaal, we verify whether or not the constructed timed automata satisfy the formulas and several logic inconsistencies in the original standard are detected and corrected. Then, we apply the code generation tool Times to generate C code from the verified model, which is later synthesized into a real MVBC chip, with some handwriting glue code. Furthermore, the runtime verification tool RMOR is applied on the integrated code, to verify some safety requirements that cannot be formalized on the timed automata. For evaluation, we compare the proposed approach with existing MVBC design methods, such as BeagleBone, Galsblock, and Simulink. Experiments show that more ambiguousness or bugs in the standard are detected during Uppaal verification, and the generated code of Times outperforms the C code generated by others in terms of the synthesized binary code size. The errors in the standard have been confirmed and the resulting MVBC has been deployed in the real train communication network.

Original languageEnglish (US)
Article number8260537
Pages (from-to)3320-3333
Number of pages14
JournalIEEE Transactions on Intelligent Transportation Systems
Issue number10
StatePublished - Oct 2018


  • IEC-61375
  • Multifunction vehicle bus
  • model-driven development
  • train communication network

ASJC Scopus subject areas

  • Automotive Engineering
  • Mechanical Engineering
  • Computer Science Applications


Dive into the research topics of 'Safety-assured model-driven design of the multifunction vehicle bus controller'. Together they form a unique fingerprint.

Cite this