On the Industrial Application of Critical Software Verification with VerCors

Marieke Huisman; Raúl E. Monti

doi:10.1007/978-3-030-61467-6_18

On the Industrial Application of Critical Software Verification with VerCors

Marieke Huisman, Raúl E. Monti

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

1 Citation (Scopus)

Abstract

Although software verification is evolving fast in both theoretical and practical aspects, it still remains absent from the actual industrial production cycle. Case studies can help to encourage these integrations. We report on our experiences applying software verification in several projects with industry. In particular, we report on two projects on the verification of tunnel control software at Technolution, where we go from a high-level design to concrete code. These case studies show the power of combining model checking (using mCRL2) and deductive verification (using VerCors) as complementary approaches. We also report on a project with Thales, where we looked at antenna bearing control software, and specified this based on their requirements documents. For all cases, we report on lessons learned and on directions for future work to improve both our tool and the industrial methodology for ensuring software correctness. Notably, our second case study involves the modelling and verification of critical software by a team of engineers from Technolution. This case study is an ongoing project; we describe our experience on the team’s learning curve for this experiment and present the preliminary conclusions on the case study.

Original language	English
Title of host publication	Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part III
Editors	Tiziana Margaria, Bernhard Steffen
Publisher	Springer Singapore
Pages	273-292
Number of pages	20
ISBN (Electronic)	978-3-030-61467-6
ISBN (Print)	978-3-030-61466-9
DOIs	https://doi.org/10.1007/978-3-030-61467-6_18
Publication status	Published - 2020
Event	9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020 - Virtual Event Duration: 20 Oct 2020 → 30 Oct 2020 Conference number: 9

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	12478

Conference

Conference	9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020
Abbreviated title	ISoLA 2020
City	Virtual Event
Period	20/10/20 → 30/10/20

Access to Document

10.1007/978-3-030-61467-6_18

Fingerprint Dive into the research topics of 'On the Industrial Application of Critical Software Verification with VerCors'. Together they form a unique fingerprint.

Cite this

Huisman, M., & Monti, R. E. (2020). On the Industrial Application of Critical Software Verification with VerCors. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part III (pp. 273-292). (Lecture Notes in Computer Science; Vol. 12478). Springer Singapore. https://doi.org/10.1007/978-3-030-61467-6_18

Huisman, Marieke ; Monti, Raúl E. / On the Industrial Application of Critical Software Verification with VerCors. Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part III. editor / Tiziana Margaria ; Bernhard Steffen. Springer Singapore, 2020. pp. 273-292 (Lecture Notes in Computer Science).

@inproceedings{07ffc08fe9574e84b030976bb4528974,

title = "On the Industrial Application of Critical Software Verification with VerCors",

abstract = "Although software verification is evolving fast in both theoretical and practical aspects, it still remains absent from the actual industrial production cycle. Case studies can help to encourage these integrations. We report on our experiences applying software verification in several projects with industry. In particular, we report on two projects on the verification of tunnel control software at Technolution, where we go from a high-level design to concrete code. These case studies show the power of combining model checking (using mCRL2) and deductive verification (using VerCors) as complementary approaches. We also report on a project with Thales, where we looked at antenna bearing control software, and specified this based on their requirements documents. For all cases, we report on lessons learned and on directions for future work to improve both our tool and the industrial methodology for ensuring software correctness. Notably, our second case study involves the modelling and verification of critical software by a team of engineers from Technolution. This case study is an ongoing project; we describe our experience on the team{\textquoteright}s learning curve for this experiment and present the preliminary conclusions on the case study.",

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

year = "2020",

doi = "10.1007/978-3-030-61467-6_18",

language = "English",

isbn = "978-3-030-61466-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer Singapore",

pages = "273--292",

editor = "Tiziana Margaria and Bernhard Steffen",

booktitle = "Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part III",

address = "Singapore",

note = "9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, ISoLA 2020 ; Conference date: 20-10-2020 Through 30-10-2020",

}

Huisman, M & Monti, RE 2020, On the Industrial Application of Critical Software Verification with VerCors. in T Margaria & B Steffen (eds), Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part III. Lecture Notes in Computer Science, vol. 12478, Springer Singapore, pp. 273-292, 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Virtual Event, 20/10/20. https://doi.org/10.1007/978-3-030-61467-6_18

On the Industrial Application of Critical Software Verification with VerCors. / Huisman, Marieke; Monti, Raúl E.

Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part III. ed. / Tiziana Margaria; Bernhard Steffen. Springer Singapore, 2020. p. 273-292 (Lecture Notes in Computer Science; Vol. 12478).

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

TY - GEN

T1 - On the Industrial Application of Critical Software Verification with VerCors

AU - Huisman, Marieke

AU - Monti, Raúl E.

N1 - Conference code: 9

PY - 2020

Y1 - 2020

N2 - Although software verification is evolving fast in both theoretical and practical aspects, it still remains absent from the actual industrial production cycle. Case studies can help to encourage these integrations. We report on our experiences applying software verification in several projects with industry. In particular, we report on two projects on the verification of tunnel control software at Technolution, where we go from a high-level design to concrete code. These case studies show the power of combining model checking (using mCRL2) and deductive verification (using VerCors) as complementary approaches. We also report on a project with Thales, where we looked at antenna bearing control software, and specified this based on their requirements documents. For all cases, we report on lessons learned and on directions for future work to improve both our tool and the industrial methodology for ensuring software correctness. Notably, our second case study involves the modelling and verification of critical software by a team of engineers from Technolution. This case study is an ongoing project; we describe our experience on the team’s learning curve for this experiment and present the preliminary conclusions on the case study.

AB - Although software verification is evolving fast in both theoretical and practical aspects, it still remains absent from the actual industrial production cycle. Case studies can help to encourage these integrations. We report on our experiences applying software verification in several projects with industry. In particular, we report on two projects on the verification of tunnel control software at Technolution, where we go from a high-level design to concrete code. These case studies show the power of combining model checking (using mCRL2) and deductive verification (using VerCors) as complementary approaches. We also report on a project with Thales, where we looked at antenna bearing control software, and specified this based on their requirements documents. For all cases, we report on lessons learned and on directions for future work to improve both our tool and the industrial methodology for ensuring software correctness. Notably, our second case study involves the modelling and verification of critical software by a team of engineers from Technolution. This case study is an ongoing project; we describe our experience on the team’s learning curve for this experiment and present the preliminary conclusions on the case study.

U2 - 10.1007/978-3-030-61467-6_18

DO - 10.1007/978-3-030-61467-6_18

M3 - Conference contribution

SN - 978-3-030-61466-9

T3 - Lecture Notes in Computer Science

SP - 273

EP - 292

BT - Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part III

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

PB - Springer Singapore

T2 - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020

Y2 - 20 October 2020 through 30 October 2020

ER -

Huisman M, Monti RE. On the Industrial Application of Critical Software Verification with VerCors. In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part III. Springer Singapore. 2020. p. 273-292. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-030-61467-6_18