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

Yu Jiang, Han Liu, Houbing Song, Hui Kong, Ming Gu, Jiaguang Sun, Lui Sha

Research output: Chapter in Book/Report/Conference proceedingConference contribution


In this paper, we present a formal model-driven engineering approach to establishing a safety-assured implementation of Multifunction vehicle bus controller (MVBC) based on the generic reference models and requirements described in the International Electrotechnical Commission (IEC) standard IEC-61375. First, the generic models described in IEC-61375 are translated into a network of timed automata, and some safety requirements tested in IEC-61375 are formalized as timed computation tree logic (TCTL) formulas. With the help of Uppaal, we check and debug whether the timed automata satisfy the formulas or not. Within this step, several logic inconsistencies in the original standard are detected and corrected. Then, we apply the tool Times to generate C code from the verified model, which was later synthesized into a real MVBC chip. Finally, the runtime verification tool RMOR is applied to verify some safety requirements at the implementation level. We set up a real platform with worldwide mostly used MVBC D113, and verify the correctness and the scalability of the synthesized MVBC chip more comprehensively. The errors in the standard has been confirmed and the resulted MVBC has been deployed in real train communication network.

Original languageEnglish (US)
Title of host publicationFM 2016
Subtitle of host publicationFormal Methods - 21st International Symposium, Proceedings
EditorsConstance Heitmeyer, Anna Philippou, Stefania Gnesi, John Fitzgerald
Number of pages7
ISBN (Print)9783319489889
StatePublished - 2016
Event21st International Symposium on Formal Methods, FM 2016 - Limassol, Cyprus
Duration: Nov 9 2016Nov 11 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9995 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other21st International Symposium on Formal Methods, FM 2016

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


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

Cite this