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

Jiang, Yu and Liu, Han and Song, Houbing and Kong, Hui and Gu, Ming and Sun, Jiaguang and Sha, Lui (2016) Safety assured formal model driven design of the multifunction vehicle bus controller. In: FM: International Symposium on Formal Methods, November 9-11, 2016, Limassol, Cyprus.

[img] Text
FM-Safety-Assured-Development-of-MVBC.pdf - Accepted Version
Available under License All rights reserved.
Download (274Kb)
Official URL:


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.

Item Type: Conference or Workshop Item (Paper)
Additional Information: The final publication is available at Springer via
Subjects: 000 Computer science, knowledge & general works > 000 Computer science, knowledge & systems > 004 Data processing & computer science
Research Group: Henzinger Group
SWORD Depositor: Sword Import User
Depositing User: Sword Import User
Date Deposited: 03 Mar 2017 07:33
Last Modified: 21 Dec 2017 12:13

Actions (login required)

View Item View Item