TY - GEN
T1 - Safety-assured formal model-driven design of the multifunction vehicle bus controller
AU - Jiang, Yu
AU - Liu, Han
AU - Song, Houbing
AU - Kong, Hui
AU - Gu, Ming
AU - Sun, Jiaguang
AU - Sha, Lui
N1 - Funding Information:
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.
Publisher Copyright:
© Springer International Publishing AG 2016.
PY - 2016
Y1 - 2016
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84996567121&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84996567121&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-48989-6_47
DO - 10.1007/978-3-319-48989-6_47
M3 - Conference contribution
AN - SCOPUS:84996567121
SN - 9783319489889
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 757
EP - 763
BT - FM 2016
A2 - Heitmeyer, Constance
A2 - Philippou, Anna
A2 - Gnesi, Stefania
A2 - Fitzgerald, John
PB - Springer
T2 - 21st International Symposium on Formal Methods, FM 2016
Y2 - 9 November 2016 through 11 November 2016
ER -