On Deductive Verification of an Industrial Concurrent Software Component with VerCors

Raúl E. Monti; Robert Rubbens; Marieke Huisman

doi:10.1007/978-3-031-19849-6_29

On Deductive Verification of an Industrial Concurrent Software Component with VerCors

Raúl E. Monti^*, Robert Rubbens, Marieke Huisman

^*Corresponding author for this work

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

2 Citations (Scopus)

79 Downloads (Pure)

Abstract

This paper presents a case study where a concurrent module of a tunnel control system written in Java is verified for memory safety and data race freedom using VerCors, a software verification tool. This case study was carried out in close collaboration with our industrial partner Technolution, which is in charge of developing the tunnel control software. First, we describe the process of preparing the code for verification, and how we make use of the different capabilities of VerCors to successfully verify the module. The concurrent module has gone through a rigorous process of design, code reviewing and unit and integration testing. Despite this careful approach, VerCors found two memory related bugs. We describe these bugs, and show how VerCors could have found them during the development process. Second, we wanted to communicate back our results and verification process to the engineers of Technolution. We discuss how we prepared our presentation, and the explanation we settled on. Third, we present interesting feedback points from this presentation. We use this feedback to determine future work directions with the goal to improve our tool support, and to bridge the gap between formal methods and industry.

Original language	English
Title of host publication	Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles
Subtitle of host publication	11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Proceedings, Part I
Editors	Tiziana Margaria, Bernhard Steffen
Pages	517-534
Number of pages	18
ISBN (Electronic)	978-3-031-19849-6
DOIs	https://doi.org/10.1007/978-3-031-19849-6_29
Publication status	Published - 17 Oct 2022
Event	11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022 - Rhodes, Greece Duration: 22 Oct 2022 → 30 Oct 2022 Conference number: 11

Conference

Conference	11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022
Abbreviated title	ISoLA 2022
Country/Territory	Greece
City	Rhodes
Period	22/10/22 → 30/10/22

Access to Document

10.1007/978-3-031-19849-6_29Licence: CC BY

978-3-031-19849-6_29Final published version, 278 KBLicence: CC BY

Cite this

Monti, R. E., Rubbens, R., & Huisman, M. (2022). On Deductive Verification of an Industrial Concurrent Software Component with VerCors. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles : 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Proceedings, Part I (pp. 517-534) https://doi.org/10.1007/978-3-031-19849-6_29

Monti, Raúl E. ; Rubbens, Robert ; Huisman, Marieke. / On Deductive Verification of an Industrial Concurrent Software Component with VerCors. Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles : 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Proceedings, Part I. editor / Tiziana Margaria ; Bernhard Steffen. 2022. pp. 517-534

@inbook{aa66597a01ae4cb1bca71a798de3bf89,

title = "On Deductive Verification of an Industrial Concurrent Software Component with VerCors",

abstract = "This paper presents a case study where a concurrent module of a tunnel control system written in Java is verified for memory safety and data race freedom using VerCors, a software verification tool. This case study was carried out in close collaboration with our industrial partner Technolution, which is in charge of developing the tunnel control software. First, we describe the process of preparing the code for verification, and how we make use of the different capabilities of VerCors to successfully verify the module. The concurrent module has gone through a rigorous process of design, code reviewing and unit and integration testing. Despite this careful approach, VerCors found two memory related bugs. We describe these bugs, and show how VerCors could have found them during the development process. Second, we wanted to communicate back our results and verification process to the engineers of Technolution. We discuss how we prepared our presentation, and the explanation we settled on. Third, we present interesting feedback points from this presentation. We use this feedback to determine future work directions with the goal to improve our tool support, and to bridge the gap between formal methods and industry.",

author = "Monti, {Ra{\'u}l E.} and Robert Rubbens and Marieke Huisman",

note = "Financial transaction number: 2500026045 ; 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022, ISoLA 2022 ; Conference date: 22-10-2022 Through 30-10-2022",

year = "2022",

month = oct,

day = "17",

doi = "10.1007/978-3-031-19849-6_29",

language = "English",

isbn = "978-3-031-19848-9",

pages = "517--534",

editor = "Tiziana Margaria and Bernhard Steffen",

booktitle = "Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles",

}

Monti, RE, Rubbens, R & Huisman, M 2022, On Deductive Verification of an Industrial Concurrent Software Component with VerCors. in T Margaria & B Steffen (eds), Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles : 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Proceedings, Part I. pp. 517-534, 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022, Rhodes, Greece, 22/10/22. https://doi.org/10.1007/978-3-031-19849-6_29

On Deductive Verification of an Industrial Concurrent Software Component with VerCors. / Monti, Raúl E.; Rubbens, Robert ; Huisman, Marieke.
Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles : 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Proceedings, Part I. ed. / Tiziana Margaria; Bernhard Steffen. 2022. p. 517-534.

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

TY - CHAP

T1 - On Deductive Verification of an Industrial Concurrent Software Component with VerCors

AU - Monti, Raúl E.

AU - Rubbens, Robert

AU - Huisman, Marieke

N1 - Conference code: 11

PY - 2022/10/17

Y1 - 2022/10/17

N2 - This paper presents a case study where a concurrent module of a tunnel control system written in Java is verified for memory safety and data race freedom using VerCors, a software verification tool. This case study was carried out in close collaboration with our industrial partner Technolution, which is in charge of developing the tunnel control software. First, we describe the process of preparing the code for verification, and how we make use of the different capabilities of VerCors to successfully verify the module. The concurrent module has gone through a rigorous process of design, code reviewing and unit and integration testing. Despite this careful approach, VerCors found two memory related bugs. We describe these bugs, and show how VerCors could have found them during the development process. Second, we wanted to communicate back our results and verification process to the engineers of Technolution. We discuss how we prepared our presentation, and the explanation we settled on. Third, we present interesting feedback points from this presentation. We use this feedback to determine future work directions with the goal to improve our tool support, and to bridge the gap between formal methods and industry.

AB - This paper presents a case study where a concurrent module of a tunnel control system written in Java is verified for memory safety and data race freedom using VerCors, a software verification tool. This case study was carried out in close collaboration with our industrial partner Technolution, which is in charge of developing the tunnel control software. First, we describe the process of preparing the code for verification, and how we make use of the different capabilities of VerCors to successfully verify the module. The concurrent module has gone through a rigorous process of design, code reviewing and unit and integration testing. Despite this careful approach, VerCors found two memory related bugs. We describe these bugs, and show how VerCors could have found them during the development process. Second, we wanted to communicate back our results and verification process to the engineers of Technolution. We discuss how we prepared our presentation, and the explanation we settled on. Third, we present interesting feedback points from this presentation. We use this feedback to determine future work directions with the goal to improve our tool support, and to bridge the gap between formal methods and industry.

U2 - 10.1007/978-3-031-19849-6_29

DO - 10.1007/978-3-031-19849-6_29

M3 - Chapter

SN - 978-3-031-19848-9

SP - 517

EP - 534

BT - Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

T2 - 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022

Y2 - 22 October 2022 through 30 October 2022

ER -

Monti RE, Rubbens R , Huisman M. On Deductive Verification of an Industrial Concurrent Software Component with VerCors. In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles : 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Proceedings, Part I. 2022. p. 517-534 doi: 10.1007/978-3-031-19849-6_29

On Deductive Verification of an Industrial Concurrent Software Component with VerCors

Abstract

Conference

Access to Document

Fingerprint

Cite this