The Library
Using threat analysis techniques to guide formal verification : a case study of cooperative awareness messages
Tools
Farrell, Marie, Bradbury, Matthew S., Fisher, Michael, Dennis, Louise A., Dixon, Claire, Yuan, Hu and Maple, Carsten (2019) Using threat analysis techniques to guide formal verification : a case study of cooperative awareness messages. In: SEFM 2019: 17th edition of the International Conference on Software Engineering and Formal Methods, Oslo, Norway, 16-20 Sep 2020. Published in: Software Engineering and Formal Methods. SEFM 2019, 11724 pp. 471-490. ISBN 9783030304454. doi:10.1007/978-3-030-30446-1_25
|
PDF
WRAP-using-threat-analysis-techniques-verification-cooperative-messages-Maple-2019.pdf - Accepted Version - Requires a PDF viewer. Download (664Kb) | Preview |
Official URL: https://doi.org/10.1007/978-3-030-30446-1_25
Abstract
Autonomous robotic systems such as Connected and Autonomous Vehicle (CAV) systems are both safety- and security-critical, since a breach in system security may impact safety. Generally, safety and security concerns for such systems are treated separately during the development process. In this paper, we consider an algorithm for sending Cooperative Awareness Messages (CAMs) between vehicles in a CAV system and the use of CAMs in preventing vehicle collisions. We employ threat analysis techniques that are commonly used in the cyber security domain to guide our formal verification. This allows us to focus our formal methods on those security properties that are particularly important and to consider both safety and security in tandem. Our analysis centres on identifying STRIDE security properties and we illustrate how these can be formalised, and subsequently verified, using a combination of formal tools for distinct aspects, namely Promela/SPIN and Dafny.
Item Type: | Conference Item (Paper) | ||||||
---|---|---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||||
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science Faculty of Science, Engineering and Medicine > Engineering > WMG (Formerly the Warwick Manufacturing Group) |
||||||
Series Name: | Lecture Notes in Computer Science | ||||||
Journal or Publication Title: | Software Engineering and Formal Methods. SEFM 2019 | ||||||
Publisher: | Springer Nature | ||||||
ISBN: | 9783030304454 | ||||||
Editor: | Ölveczky, P. and Salaün , G. | ||||||
Official Date: | 9 September 2019 | ||||||
Dates: |
|
||||||
Volume: | 11724 | ||||||
Page Range: | pp. 471-490 | ||||||
DOI: | 10.1007/978-3-030-30446-1_25 | ||||||
Status: | Peer Reviewed | ||||||
Publication Status: | Published | ||||||
Reuse Statement (publisher, data, author rights): | This is a post-peer-review, pre-copyedit version of an article published in Software Engineering and Formal Methods. SEFM 2019. The final authenticated version is available online at: https://doi.org/10.1007/978-3-030-30446-1_25 | ||||||
Access rights to Published version: | Restricted or Subscription Access | ||||||
Copyright Holders: | © Springer Nature Switzerland AG 2019 | ||||||
Date of first compliant deposit: | 9 September 2019 | ||||||
Date of first compliant Open Access: | 16 September 2019 | ||||||
Funder: | FAIR-SPACE Hub | ||||||
Grant number: | EP/R026092 | ||||||
Conference Paper Type: | Paper | ||||||
Title of Event: | SEFM 2019: 17th edition of the International Conference on Software Engineering and Formal Methods | ||||||
Type of Event: | Conference | ||||||
Location of Event: | Oslo, Norway | ||||||
Date(s) of Event: | 16-20 Sep 2020 | ||||||
Related URLs: |
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |
Downloads
Downloads per month over past year