--- _id: '1205' abstract: - lang: eng text: 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. acknowledgement: "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.\r\n" alternative_title: - LNCS author: - first_name: Yu full_name: Jiang, Yu last_name: Jiang - first_name: Han full_name: Liu, Han last_name: Liu - first_name: Houbing full_name: Song, Houbing last_name: Song - first_name: Hui full_name: Kong, Hui id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87 last_name: Kong orcid: 0000-0002-3066-6941 - first_name: Ming full_name: Gu, Ming last_name: Gu - first_name: Jiaguang full_name: Sun, Jiaguang last_name: Sun - first_name: Lui full_name: Sha, Lui last_name: Sha citation: ama: 'Jiang Y, Liu H, Song H, et al. Safety assured formal model driven design of the multifunction vehicle bus controller. In: Vol 9995. Springer; 2016:757-763. doi:10.1007/978-3-319-48989-6_47' apa: 'Jiang, Y., Liu, H., Song, H., Kong, H., Gu, M., Sun, J., & Sha, L. (2016). Safety assured formal model driven design of the multifunction vehicle bus controller (Vol. 9995, pp. 757–763). Presented at the FM: International Symposium on Formal Methods, Limassol, Cyprus: Springer. https://doi.org/10.1007/978-3-319-48989-6_47' chicago: Jiang, Yu, Han Liu, Houbing Song, Hui Kong, Ming Gu, Jiaguang Sun, and Lui Sha. “Safety Assured Formal Model Driven Design of the Multifunction Vehicle Bus Controller,” 9995:757–63. Springer, 2016. https://doi.org/10.1007/978-3-319-48989-6_47. ieee: 'Y. Jiang et al., “Safety assured formal model driven design of the multifunction vehicle bus controller,” presented at the FM: International Symposium on Formal Methods, Limassol, Cyprus, 2016, vol. 9995, pp. 757–763.' ista: 'Jiang Y, Liu H, Song H, Kong H, Gu M, Sun J, Sha L. 2016. Safety assured formal model driven design of the multifunction vehicle bus controller. FM: International Symposium on Formal Methods, LNCS, vol. 9995, 757–763.' mla: Jiang, Yu, et al. Safety Assured Formal Model Driven Design of the Multifunction Vehicle Bus Controller. Vol. 9995, Springer, 2016, pp. 757–63, doi:10.1007/978-3-319-48989-6_47. short: Y. Jiang, H. Liu, H. Song, H. Kong, M. Gu, J. Sun, L. Sha, in:, Springer, 2016, pp. 757–763. conference: end_date: 2016-11-11 location: Limassol, Cyprus name: 'FM: International Symposium on Formal Methods' start_date: 2016-11-09 date_created: 2018-12-11T11:50:42Z date_published: 2016-11-08T00:00:00Z date_updated: 2023-09-18T08:12:48Z day: '08' ddc: - '004' department: - _id: ToHe doi: 10.1007/978-3-319-48989-6_47 file: - access_level: open_access checksum: fea0b3fae9a2a42e8bfec59840e30d8c content_type: application/pdf creator: system date_created: 2018-12-12T10:08:13Z date_updated: 2020-07-14T12:44:39Z file_id: '4673' file_name: IST-2017-783-v1+1_FM-Safety-Assured-Development-of-MVBC.pdf file_size: 281501 relation: main_file file_date_updated: 2020-07-14T12:44:39Z has_accepted_license: '1' intvolume: ' 9995' language: - iso: eng month: '11' oa: 1 oa_version: Submitted Version page: 757 - 763 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize publication_status: published publisher: Springer publist_id: '6144' pubrep_id: '783' quality_controlled: '1' related_material: record: - id: '434' relation: later_version status: public scopus_import: 1 status: public title: Safety assured formal model driven design of the multifunction vehicle bus controller type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 9995 year: '2016' ...