@InProceedings{10.1007/978-3-030-61467-6_18,
author="Huisman, Marieke
and Monti, Ra{\'u}l E.",
editor="Margaria, Tiziana
and Steffen, Bernhard",
title="On the Industrial Application of Critical Software Verification with VerCors",
booktitle="Leveraging Applications of Formal Methods, Verification and Validation: Applications",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="273--292",
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.",
isbn="978-3-030-61467-6",
url = {https://doi.org/10.1007/978-3-030-61467-6_18}
}

{"_id":"rmonxv3dxXf4spJTg","bibbaseid":"huisman-monti-ontheindustrialapplicationofcriticalsoftwareverificationwithvercors-2020","authorIDs":[],"author_short":["Huisman, M.","Monti, R. E."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Huisman"],"firstnames":["Marieke"],"suffixes":[]},{"propositions":[],"lastnames":["Monti"],"firstnames":["Raúl","E."],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Margaria"],"firstnames":["Tiziana"],"suffixes":[]},{"propositions":[],"lastnames":["Steffen"],"firstnames":["Bernhard"],"suffixes":[]}],"title":"On the Industrial Application of Critical Software Verification with VerCors","booktitle":"Leveraging Applications of Formal Methods, Verification and Validation: Applications","year":"2020","publisher":"Springer International Publishing","address":"Cham","pages":"273–292","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.","isbn":"978-3-030-61467-6","url":"https://doi.org/10.1007/978-3-030-61467-6_18","bibtex":"@InProceedings{10.1007/978-3-030-61467-6_18,\nauthor=\"Huisman, Marieke\nand Monti, Ra{\\'u}l E.\",\neditor=\"Margaria, Tiziana\nand Steffen, Bernhard\",\ntitle=\"On the Industrial Application of Critical Software Verification with VerCors\",\nbooktitle=\"Leveraging Applications of Formal Methods, Verification and Validation: Applications\",\nyear=\"2020\",\npublisher=\"Springer International Publishing\",\naddress=\"Cham\",\npages=\"273--292\",\nabstract=\"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.\",\nisbn=\"978-3-030-61467-6\",\nurl = {https://doi.org/10.1007/978-3-030-61467-6_18}\n}\n\n\n","author_short":["Huisman, M.","Monti, R. E."],"editor_short":["Margaria, T.","Steffen, B."],"key":"10.1007/978-3-030-61467-6_18","id":"10.1007/978-3-030-61467-6_18","bibbaseid":"huisman-monti-ontheindustrialapplicationofcriticalsoftwareverificationwithvercors-2020","role":"author","urls":{"Paper":"https://doi.org/10.1007/978-3-030-61467-6_18"},"metadata":{"authorlinks":{}},"downloads":6},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/utwente-fmt/vercors-web/master/static/references.bib","creationDate":"2021-03-09T09:33:20.563Z","downloads":6,"keywords":[],"search_terms":["industrial","application","critical","software","verification","vercors","huisman","monti"],"title":"On the Industrial Application of Critical Software Verification with VerCors","year":2020,"dataSources":["2tJugFYAignELAmZo","zT4KxAXTKvhK2Hrr4","cCvCnPTRQYq3qPe9y"]}