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

Author(s): Jiang, Yu; Liu, Han; Song, Houbing; Kong, Hui; Gu, Ming; Sun, Jiaguang; Sha, Lui
Title: Safety assured formal model driven design of the multifunction vehicle bus controller
Title Series: LNCS
Affiliation IST Austria
Abstract: 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.
Conference Title: FM: International Symposium on Formal Methods
Volume: 9995
Conference Dates: November 9-11, 2016
Conference Location: Limassol, Cyprus
ISBN: 978-331948988-9
Publisher: Springer  
Date Published: 2016-01-01
Start Page: 757
End Page: 763
DOI: 10.1007/978-3-319-48989-6_47
Notes: This research is sponsored in part by NSFC Program (No. 91218302, No. 61527812), National Science and Technology Major Project (No. 2016ZX01038101), Tsinghua University Initiative Scientific Research Program (20131089331), MIIT IT funds (Research and application of TCN key technologies) of China, and the National Key Technology R&D Program (No. 2015BAG14B01-02), Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23.
Open access: yes (repository)
IST Austria Authors
  1. Hui Kong
    9 Kong
Related IST Austria Work