An Approach to Formal Verification of Autonomous Vehicle Systems using Threat Analysis

Sheraz Mazhar; Abdur Rakib; Robin Doss; Adnan Anwar

doi:10.1109/ICVES65691.2025.11376182

An Approach to Formal Verification of Autonomous Vehicle Systems using Threat Analysis

Sheraz Mazhar
, Abdur Rakib
, Robin Doss
, Adnan Anwar

Centre for Future Transport and Cities

Deakin University

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

38 Downloads (Pure)

Abstract

The rapid advancement and deployment of connected and autonomous vehicles (CAVs) present transformative opportunities to enhance safety, efficiency, and convenience within the transportation industry. However, these innovations introduce significant cybersecurity risks due to the complex electronics and continuous connectivity that CAVs depend on. Traditional testing methods, while critical, often fall short in detecting vulnerabilities across the vast range of scenarios these vehicles may encounter. Formal verification, a mathematical approach to system validation, offers a more rigorous and comprehensive solution by ensuring that systems operate as expected to search through all possible execution paths. However, defining appropriate system properties for verification remains a challenge, as a system designer may write properties that fail to address real-world threats effectively. This research addresses this gap by integrating threat analysis into the process of defining security properties, ensuring that the verification process is aligned with actual cybersecurity risks. We leverage Natural Language Processing (NLP) to extract key security details from threat analysis result texts, automating the generation of system properties. This approach simplifies the verification process, with its usability demonstrated through a high-level 5G-V2X design use case scenario.

Original language	English
Title of host publication	2025 IEEE International Conference on Vehicular Electronics and Safety (ICVES)
Publisher	IEEE
Pages	437-444
Number of pages	8
ISBN (Electronic)	978-1-6654-7778-9
ISBN (Print)	978-1-6654-7779-6
DOIs	https://doi.org/10.1109/ICVES65691.2025.11376182
Publication status	E-pub ahead of print - 11 Feb 2026
Event	19th IEEE International Conference on Vehicular Electronics and Safety - Coventry, United Kingdom Duration: 27 Oct 2025 → 28 Oct 2025

Conference

Conference	19th IEEE International Conference on Vehicular Electronics and Safety
Abbreviated title	ICVES2025
Country/Territory	United Kingdom
City	Coventry
Period	27/10/25 → 28/10/25

Bibliographical note

© 2025 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.

Copyright © and Moral Rights are retained by the author(s) and/ or other copyright owners. A copy can be downloaded for personal non-commercial research or study, without prior permission or charge. This item cannot be reproduced or quoted extensively from without first obtaining permission in writing from the copyright holder(s). The content must not be changed in any way or sold commercially in any format or medium without the formal permission of the copyright holders.

This document is the author’s post-print version, incorporating any revisions agreed during the peer-review process. Some differences between the published version and this version may remain and you are advised to consult the published version if you wish to cite from it.

Keywords

Automotive Cybersecurity
Inter-Vehicular Communication
Threat Analysis
Formal Verification

Access to Document

10.1109/ICVES65691.2025.11376182

Mazhar2025AAMAccepted author manuscript, 1.05 MBLicence: CC BY-NC-ND

Cite this

Mazhar, S, Rakib, A, Doss, R & Anwar, A 2026, An Approach to Formal Verification of Autonomous Vehicle Systems using Threat Analysis. in 2025 IEEE International Conference on Vehicular Electronics and Safety (ICVES). IEEE, pp. 437-444, 19th IEEE International Conference on Vehicular Electronics and Safety, Coventry, United Kingdom, 27/10/25. https://doi.org/10.1109/ICVES65691.2025.11376182

@inproceedings{5299f54831ef4f8ca8f168aef98c82e8,

title = "An Approach to Formal Verification of Autonomous Vehicle Systems using Threat Analysis",

abstract = "The rapid advancement and deployment of connected and autonomous vehicles (CAVs) present transformative opportunities to enhance safety, efficiency, and convenience within the transportation industry. However, these innovations introduce significant cybersecurity risks due to the complex electronics and continuous connectivity that CAVs depend on. Traditional testing methods, while critical, often fall short in detecting vulnerabilities across the vast range of scenarios these vehicles may encounter. Formal verification, a mathematical approach to system validation, offers a more rigorous and comprehensive solution by ensuring that systems operate as expected to search through all possible execution paths. However, defining appropriate system properties for verification remains a challenge, as a system designer may write properties that fail to address real-world threats effectively. This research addresses this gap by integrating threat analysis into the process of defining security properties, ensuring that the verification process is aligned with actual cybersecurity risks. We leverage Natural Language Processing (NLP) to extract key security details from threat analysis result texts, automating the generation of system properties. This approach simplifies the verification process, with its usability demonstrated through a high-level 5G-V2X design use case scenario.",

keywords = "Automotive Cybersecurity, Inter-Vehicular Communication, Threat Analysis, Formal Verification",

author = "Sheraz Mazhar and Abdur Rakib and Robin Doss and Adnan Anwar",

note = "{\textcopyright} 2025 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works. Copyright {\textcopyright} and Moral Rights are retained by the author(s) and/ or other copyright owners. A copy can be downloaded for personal non-commercial research or study, without prior permission or charge. This item cannot be reproduced or quoted extensively from without first obtaining permission in writing from the copyright holder(s). The content must not be changed in any way or sold commercially in any format or medium without the formal permission of the copyright holders. This document is the author{\textquoteright}s post-print version, incorporating any revisions agreed during the peer-review process. Some differences between the published version and this version may remain and you are advised to consult the published version if you wish to cite from it. ; 19th IEEE International Conference on Vehicular Electronics and Safety, ICVES2025 ; Conference date: 27-10-2025 Through 28-10-2025",

year = "2026",

month = feb,

day = "11",

doi = "10.1109/ICVES65691.2025.11376182",

language = "English",

isbn = "978-1-6654-7779-6",

pages = "437--444",

booktitle = "2025 IEEE International Conference on Vehicular Electronics and Safety (ICVES)",

publisher = "IEEE",

address = "United States",

}

TY - GEN

T1 - An Approach to Formal Verification of Autonomous Vehicle Systems using Threat Analysis

AU - Mazhar, Sheraz

AU - Rakib, Abdur

AU - Doss, Robin

AU - Anwar, Adnan

N1 - © 2025 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works. Copyright © and Moral Rights are retained by the author(s) and/ or other copyright owners. A copy can be downloaded for personal non-commercial research or study, without prior permission or charge. This item cannot be reproduced or quoted extensively from without first obtaining permission in writing from the copyright holder(s). The content must not be changed in any way or sold commercially in any format or medium without the formal permission of the copyright holders. This document is the author’s post-print version, incorporating any revisions agreed during the peer-review process. Some differences between the published version and this version may remain and you are advised to consult the published version if you wish to cite from it.

PY - 2026/2/11

Y1 - 2026/2/11

N2 - The rapid advancement and deployment of connected and autonomous vehicles (CAVs) present transformative opportunities to enhance safety, efficiency, and convenience within the transportation industry. However, these innovations introduce significant cybersecurity risks due to the complex electronics and continuous connectivity that CAVs depend on. Traditional testing methods, while critical, often fall short in detecting vulnerabilities across the vast range of scenarios these vehicles may encounter. Formal verification, a mathematical approach to system validation, offers a more rigorous and comprehensive solution by ensuring that systems operate as expected to search through all possible execution paths. However, defining appropriate system properties for verification remains a challenge, as a system designer may write properties that fail to address real-world threats effectively. This research addresses this gap by integrating threat analysis into the process of defining security properties, ensuring that the verification process is aligned with actual cybersecurity risks. We leverage Natural Language Processing (NLP) to extract key security details from threat analysis result texts, automating the generation of system properties. This approach simplifies the verification process, with its usability demonstrated through a high-level 5G-V2X design use case scenario.

AB - The rapid advancement and deployment of connected and autonomous vehicles (CAVs) present transformative opportunities to enhance safety, efficiency, and convenience within the transportation industry. However, these innovations introduce significant cybersecurity risks due to the complex electronics and continuous connectivity that CAVs depend on. Traditional testing methods, while critical, often fall short in detecting vulnerabilities across the vast range of scenarios these vehicles may encounter. Formal verification, a mathematical approach to system validation, offers a more rigorous and comprehensive solution by ensuring that systems operate as expected to search through all possible execution paths. However, defining appropriate system properties for verification remains a challenge, as a system designer may write properties that fail to address real-world threats effectively. This research addresses this gap by integrating threat analysis into the process of defining security properties, ensuring that the verification process is aligned with actual cybersecurity risks. We leverage Natural Language Processing (NLP) to extract key security details from threat analysis result texts, automating the generation of system properties. This approach simplifies the verification process, with its usability demonstrated through a high-level 5G-V2X design use case scenario.

KW - Automotive Cybersecurity

KW - Inter-Vehicular Communication

KW - Threat Analysis

KW - Formal Verification

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

U2 - 10.1109/ICVES65691.2025.11376182

DO - 10.1109/ICVES65691.2025.11376182

M3 - Conference proceeding

SN - 978-1-6654-7779-6

SP - 437

EP - 444

BT - 2025 IEEE International Conference on Vehicular Electronics and Safety (ICVES)

PB - IEEE

T2 - 19th IEEE International Conference on Vehicular Electronics and Safety

Y2 - 27 October 2025 through 28 October 2025

ER -

An Approach to Formal Verification of Autonomous Vehicle Systems using Threat Analysis

Abstract

Conference

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this