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 proceedingChapterAcademicpeer-review

2 Citations (Scopus)
52 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 languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation. Verification Principles
Subtitle of host publication11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Proceedings, Part I
EditorsTiziana Margaria, Bernhard Steffen
Pages517-534
Number of pages18
ISBN (Electronic)978-3-031-19849-6
DOIs
Publication statusPublished - 17 Oct 2022
Event11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022 - Rhodes, Greece
Duration: 22 Oct 202230 Oct 2022
Conference number: 11

Conference

Conference11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022
Abbreviated titleISoLA 2022
Country/TerritoryGreece
CityRhodes
Period22/10/2230/10/22

Fingerprint

Dive into the research topics of 'On Deductive Verification of an Industrial Concurrent Software Component with VerCors'. Together they form a unique fingerprint.

Cite this