Enhancing the Formal Verification of Train Control Systems based on Decomposition

Tengfei Li; Junfeng Sun; Xinjun Lv; Xiang Chen; Jing Liu; Haiying Sun

doi:10.1109/COMPSAC57700.2023.00279

Enhancing the Formal Verification of Train Control Systems based on Decomposition

Tengfei Li
, Junfeng Sun^*
, Xinjun Lv
, Xiang Chen
, Jing Liu^*
, Haiying Sun

^*此作品的通讯作者

软件工程学院

Casco Signal Ltd
East China Normal University

科研成果: 书/报告/会议事项章节 › 会议稿件 › 同行评审

摘要

Great achievements have improved the efficiency and effectiveness of formal verification fairly, such that it is now applicable to industrial-scale software. However, verifying a full software system is still considered too complex. In practice, industrial control software models to be verified may result in state space explosion. We propose a problem frame-based approach that takes the full software system as input and tries to decompose the full software model into some smaller modules. Our approach decomposes the whole safety requirements to sub safety requirements, and the verification problem of the whole model is projected to sub verification problem according to the decomposed safety requirements. The sub verification problems check the projected sub models against the the sub safety requirements. We carry out an extensive evaluation based on the trackside subsystems in rail transit. Verifying the decomposed model can lead to a significant performance gain, due to the fact that abstract models reduce too much state space.

源语言	英语
主期刊名	Proceedings - 2023 IEEE 47th Annual Computers, Software, and Applications Conference, COMPSAC 2023
编辑	Hossain Shahriar, Yuuichi Teranishi, Alfredo Cuzzocrea, Moushumi Sharmin, Dave Towey, AKM Jahangir Alam Majumder, Hiroki Kashiwazaki, Ji-Jiang Yang, Michiharu Takemoto, Nazmus Sakib, Ryohei Banno, Sheikh Iqbal Ahamed
出版商	IEEE Computer Society
页	1804-1809
页数	6
ISBN（电子版）	9798350326970
DOI	https://doi.org/10.1109/COMPSAC57700.2023.00279
出版状态	已出版 - 2023
活动	47th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2023 - Hybrid, Torino, 意大利期限: 26 6月 2023 → 30 6月 2023

出版系列

姓名	Proceedings - International Computer Software and Applications Conference
卷	2023-June
ISSN（印刷版）	0730-3157

会议

会议	47th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2023
国家/地区	意大利
市	Hybrid, Torino
时期	26/06/23 → 30/06/23

访问文件

10.1109/COMPSAC57700.2023.00279

其它文件与链接

链接到 Scopus 的出版物

引用此

Li, T., Sun, J., Lv, X., Chen, X., Liu, J., & Sun, H. (2023). Enhancing the Formal Verification of Train Control Systems based on Decomposition. 在 H. Shahriar, Y. Teranishi, A. Cuzzocrea, M. Sharmin, D. Towey, AKM. J. A. Majumder, H. Kashiwazaki, J.-J. Yang, M. Takemoto, N. Sakib, R. Banno, & S. I. Ahamed (编辑), Proceedings - 2023 IEEE 47th Annual Computers, Software, and Applications Conference, COMPSAC 2023 (页码 1804-1809). (Proceedings - International Computer Software and Applications Conference; 卷 2023-June). IEEE Computer Society. https://doi.org/10.1109/COMPSAC57700.2023.00279

Li, Tengfei ; Sun, Junfeng ; Lv, Xinjun 等. / Enhancing the Formal Verification of Train Control Systems based on Decomposition. Proceedings - 2023 IEEE 47th Annual Computers, Software, and Applications Conference, COMPSAC 2023. 编辑 / Hossain Shahriar ; Yuuichi Teranishi ; Alfredo Cuzzocrea ; Moushumi Sharmin ; Dave Towey ; AKM Jahangir Alam Majumder ; Hiroki Kashiwazaki ; Ji-Jiang Yang ; Michiharu Takemoto ; Nazmus Sakib ; Ryohei Banno ; Sheikh Iqbal Ahamed. IEEE Computer Society, 2023. 页码 1804-1809 (Proceedings - International Computer Software and Applications Conference).

@inproceedings{1bff6b64ff8b4e3fae9bd34961e9f640,

title = "Enhancing the Formal Verification of Train Control Systems based on Decomposition",

abstract = "Great achievements have improved the efficiency and effectiveness of formal verification fairly, such that it is now applicable to industrial-scale software. However, verifying a full software system is still considered too complex. In practice, industrial control software models to be verified may result in state space explosion. We propose a problem frame-based approach that takes the full software system as input and tries to decompose the full software model into some smaller modules. Our approach decomposes the whole safety requirements to sub safety requirements, and the verification problem of the whole model is projected to sub verification problem according to the decomposed safety requirements. The sub verification problems check the projected sub models against the the sub safety requirements. We carry out an extensive evaluation based on the trackside subsystems in rail transit. Verifying the decomposed model can lead to a significant performance gain, due to the fact that abstract models reduce too much state space.",

keywords = "Formal Verification, Problem Frame, Projection, Safety Property, Train Control Systems",

author = "Tengfei Li and Junfeng Sun and Xinjun Lv and Xiang Chen and Jing Liu and Haiying Sun",

note = "Publisher Copyright: {\textcopyright} 2023 IEEE.; 47th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2023 ; Conference date: 26-06-2023 Through 30-06-2023",

year = "2023",

doi = "10.1109/COMPSAC57700.2023.00279",

language = "英语",

series = "Proceedings - International Computer Software and Applications Conference",

publisher = "IEEE Computer Society",

pages = "1804--1809",

editor = "Hossain Shahriar and Yuuichi Teranishi and Alfredo Cuzzocrea and Moushumi Sharmin and Dave Towey and Majumder, \{AKM Jahangir Alam\} and Hiroki Kashiwazaki and Ji-Jiang Yang and Michiharu Takemoto and Nazmus Sakib and Ryohei Banno and Ahamed, \{Sheikh Iqbal\}",

booktitle = "Proceedings - 2023 IEEE 47th Annual Computers, Software, and Applications Conference, COMPSAC 2023",

address = "美国",

}

Li, T, Sun, J, Lv, X, Chen, X, Liu, J & Sun, H 2023, Enhancing the Formal Verification of Train Control Systems based on Decomposition. 在 H Shahriar, Y Teranishi, A Cuzzocrea, M Sharmin, D Towey, AKMJA Majumder, H Kashiwazaki, J-J Yang, M Takemoto, N Sakib, R Banno & SI Ahamed (编辑), Proceedings - 2023 IEEE 47th Annual Computers, Software, and Applications Conference, COMPSAC 2023. Proceedings - International Computer Software and Applications Conference, 卷 2023-June, IEEE Computer Society, 页码 1804-1809, 47th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2023, Hybrid, Torino, 意大利, 26/06/23. https://doi.org/10.1109/COMPSAC57700.2023.00279

Enhancing the Formal Verification of Train Control Systems based on Decomposition. / Li, Tengfei; Sun, Junfeng; Lv, Xinjun 等.
Proceedings - 2023 IEEE 47th Annual Computers, Software, and Applications Conference, COMPSAC 2023. 编辑 / Hossain Shahriar; Yuuichi Teranishi; Alfredo Cuzzocrea; Moushumi Sharmin; Dave Towey; AKM Jahangir Alam Majumder; Hiroki Kashiwazaki; Ji-Jiang Yang; Michiharu Takemoto; Nazmus Sakib; Ryohei Banno; Sheikh Iqbal Ahamed. IEEE Computer Society, 2023. 页码 1804-1809 (Proceedings - International Computer Software and Applications Conference; 卷 2023-June).

科研成果: 书/报告/会议事项章节 › 会议稿件 › 同行评审

TY - GEN

T1 - Enhancing the Formal Verification of Train Control Systems based on Decomposition

AU - Li, Tengfei

AU - Sun, Junfeng

AU - Lv, Xinjun

AU - Chen, Xiang

AU - Liu, Jing

AU - Sun, Haiying

PY - 2023

Y1 - 2023

N2 - Great achievements have improved the efficiency and effectiveness of formal verification fairly, such that it is now applicable to industrial-scale software. However, verifying a full software system is still considered too complex. In practice, industrial control software models to be verified may result in state space explosion. We propose a problem frame-based approach that takes the full software system as input and tries to decompose the full software model into some smaller modules. Our approach decomposes the whole safety requirements to sub safety requirements, and the verification problem of the whole model is projected to sub verification problem according to the decomposed safety requirements. The sub verification problems check the projected sub models against the the sub safety requirements. We carry out an extensive evaluation based on the trackside subsystems in rail transit. Verifying the decomposed model can lead to a significant performance gain, due to the fact that abstract models reduce too much state space.

AB - Great achievements have improved the efficiency and effectiveness of formal verification fairly, such that it is now applicable to industrial-scale software. However, verifying a full software system is still considered too complex. In practice, industrial control software models to be verified may result in state space explosion. We propose a problem frame-based approach that takes the full software system as input and tries to decompose the full software model into some smaller modules. Our approach decomposes the whole safety requirements to sub safety requirements, and the verification problem of the whole model is projected to sub verification problem according to the decomposed safety requirements. The sub verification problems check the projected sub models against the the sub safety requirements. We carry out an extensive evaluation based on the trackside subsystems in rail transit. Verifying the decomposed model can lead to a significant performance gain, due to the fact that abstract models reduce too much state space.

KW - Formal Verification

KW - Problem Frame

KW - Projection

KW - Safety Property

KW - Train Control Systems

UR - https://www.scopus.com/pages/publications/85168864598

U2 - 10.1109/COMPSAC57700.2023.00279

DO - 10.1109/COMPSAC57700.2023.00279

M3 - 会议稿件

AN - SCOPUS:85168864598

T3 - Proceedings - International Computer Software and Applications Conference

SP - 1804

EP - 1809

BT - Proceedings - 2023 IEEE 47th Annual Computers, Software, and Applications Conference, COMPSAC 2023

A2 - Shahriar, Hossain

A2 - Teranishi, Yuuichi

A2 - Cuzzocrea, Alfredo

A2 - Sharmin, Moushumi

A2 - Towey, Dave

A2 - Majumder, AKM Jahangir Alam

A2 - Kashiwazaki, Hiroki

A2 - Yang, Ji-Jiang

A2 - Takemoto, Michiharu

A2 - Sakib, Nazmus

A2 - Banno, Ryohei

A2 - Ahamed, Sheikh Iqbal

PB - IEEE Computer Society

T2 - 47th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2023

Y2 - 26 June 2023 through 30 June 2023

ER -

Li T, Sun J, Lv X, Chen X, Liu J, Sun H. Enhancing the Formal Verification of Train Control Systems based on Decomposition. 在 Shahriar H, Teranishi Y, Cuzzocrea A, Sharmin M, Towey D, Majumder AKMJA, Kashiwazaki H, Yang JJ, Takemoto M, Sakib N, Banno R, Ahamed SI, 编辑, Proceedings - 2023 IEEE 47th Annual Computers, Software, and Applications Conference, COMPSAC 2023. IEEE Computer Society. 2023. 页码 1804-1809. (Proceedings - International Computer Software and Applications Conference). doi: 10.1109/COMPSAC57700.2023.00279

Enhancing the Formal Verification of Train Control Systems based on Decomposition

摘要

出版系列

会议

访问文件

其它文件与链接

指纹

引用此