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

^*Corresponding author for this work

Software Engineering Institute

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Proceedings - 2023 IEEE 47th Annual Computers, Software, and Applications Conference, COMPSAC 2023
Editors	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
Publisher	IEEE Computer Society
Pages	1804-1809
Number of pages	6
ISBN (Electronic)	9798350326970
DOIs	https://doi.org/10.1109/COMPSAC57700.2023.00279
State	Published - 2023
Event	47th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2023 - Hybrid, Torino, Italy Duration: 26 Jun 2023 → 30 Jun 2023

Publication series

Name	Proceedings - International Computer Software and Applications Conference
Volume	2023-June
ISSN (Print)	0730-3157

Conference

Conference	47th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2023
Country/Territory	Italy
City	Hybrid, Torino
Period	26/06/23 → 30/06/23

Keywords

Formal Verification
Problem Frame
Projection
Safety Property
Train Control Systems

Access to Document

10.1109/COMPSAC57700.2023.00279

Cite this

Li, T., Sun, J., Lv, X., Chen, X., Liu, J., & Sun, H. (2023). Enhancing the Formal Verification of Train Control Systems based on Decomposition. In 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 (Eds.), Proceedings - 2023 IEEE 47th Annual Computers, Software, and Applications Conference, COMPSAC 2023 (pp. 1804-1809). (Proceedings - International Computer Software and Applications Conference; Vol. 2023-June). IEEE Computer Society. https://doi.org/10.1109/COMPSAC57700.2023.00279

Li, Tengfei ; Sun, Junfeng ; Lv, Xinjun et al. / Enhancing the Formal Verification of Train Control Systems based on Decomposition. Proceedings - 2023 IEEE 47th Annual Computers, Software, and Applications Conference, COMPSAC 2023. editor / 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. pp. 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. in 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 (eds), Proceedings - 2023 IEEE 47th Annual Computers, Software, and Applications Conference, COMPSAC 2023. Proceedings - International Computer Software and Applications Conference, vol. 2023-June, IEEE Computer Society, pp. 1804-1809, 47th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2023, Hybrid, Torino, Italy, 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 et al.
Proceedings - 2023 IEEE 47th Annual Computers, Software, and Applications Conference, COMPSAC 2023. ed. / 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. p. 1804-1809 (Proceedings - International Computer Software and Applications Conference; Vol. 2023-June).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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. In Shahriar H, Teranishi Y, Cuzzocrea A, Sharmin M, Towey D, Majumder AKMJA, Kashiwazaki H, Yang JJ, Takemoto M, Sakib N, Banno R, Ahamed SI, editors, Proceedings - 2023 IEEE 47th Annual Computers, Software, and Applications Conference, COMPSAC 2023. IEEE Computer Society. 2023. p. 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

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this