{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T16:43:53Z","timestamp":1742921033147,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031198489"},{"type":"electronic","value":"9783031198496"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,10,17]],"date-time":"2022-10-17T00:00:00Z","timestamp":1665964800000},"content-version":"vor","delay-in-days":289,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<\/jats:p>","DOI":"10.1007\/978-3-031-19849-6_29","type":"book-chapter","created":{"date-parts":[[2022,10,19]],"date-time":"2022-10-19T15:03:32Z","timestamp":1666191812000},"page":"517-534","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["On Deductive Verification of\u00a0an\u00a0Industrial Concurrent Software Component with\u00a0VerCors"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6964-1426","authenticated-orcid":false,"given":"Ra\u00fal E.","family":"Monti","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5638-5945","authenticated-orcid":false,"given":"Robert","family":"Rubbens","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4467-072X","authenticated-orcid":false,"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,10,17]]},"reference":[{"key":"29_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"757","DOI":"10.1007\/11901433_41","volume-title":"Formal Methods and Software Engineering","author":"A Bauer","year":"2006","unstructured":"Bauer, A., Leucker, M., Streit, J.: SALT\u2014structured assertion language for temporal logic. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 757\u2013775. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11901433_41"},{"key":"29_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-44585-4_33","volume-title":"Computer Aided Verification","author":"I Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 363\u2013367. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_33"},{"key":"29_CR3","unstructured":"Welkom bij de Blankenburgverbinding. https:\/\/www.blankenburgverbinding.nl\/. Accessed 21 Jan 2022"},{"key":"29_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-319-66845-1_7","volume-title":"Integrated Formal Methods","author":"S Blom","year":"2017","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: verification of parallel and concurrent software. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 102\u2013110. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_7"},{"key":"29_CR5","doi-asserted-by":"publisher","first-page":"871","DOI":"10.1007\/978-3-319-10575-8_26","volume-title":"Handbook of Model Checking","author":"J Bradfield","year":"2018","unstructured":"Bradfield, J., Walukiewicz, I.: The mu-calculus and model checking. In: Handbook of Model Checking, pp. 871\u2013919. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_26"},{"key":"29_CR6","doi-asserted-by":"publisher","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. SIGPLAN Not. 35(9), 268\u2013279 (2000). https:\/\/doi.org\/10.1145\/357766.351266","DOI":"10.1145\/357766.351266"},{"key":"29_CR7","doi-asserted-by":"publisher","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Robby: a language framework for expressing checkable properties of dynamic software. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN Model Checking and Software Verification, 7th International SPIN Workshop, Stanford, CA, USA, August 30\u2013September 1, 2000, Proceedings. LNCS, vol. 1885, pp. 205\u2013223. Springer, Cham (2000). https:\/\/doi.org\/10.1007\/10722468_13","DOI":"10.1007\/10722468_13"},{"key":"29_CR8","unstructured":"Coverity. https:\/\/www.synopsys.com\/software-integrity\/security-testing\/static-analysis-sast.html. Accessed 18 May 2022"},{"key":"29_CR9","unstructured":"Findbugs. https:\/\/findbugs.sourceforge.net\/. Accessed 18 May 2022"},{"key":"29_CR10","doi-asserted-by":"publisher","unstructured":"Haack, C., Huisman, M., Hurlin, C., Amighi, A.: Permission-based separation logic for multithreaded java programs. Log. Methods Comput. Sci. 11(1) (2015). https:\/\/doi.org\/10.2168\/LMCS-11(1:2)2015, https:\/\/lmcs.episciences.org\/998","DOI":"10.2168\/LMCS-11(1:2)2015"},{"key":"29_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-030-61467-6_18","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Applications","author":"M Huisman","year":"2020","unstructured":"Huisman, M., Monti, R.E.: On the industrial application of critical software verification with VerCors. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12478, pp. 273\u2013292. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61467-6_18"},{"key":"29_CR12","unstructured":"Hurlin, C.: Specification and Verification of Multithreaded Object-Oriented Programs with Separation Logic. Ph.D. thesis, Universit\u00e9 Nice Sophia Antipolis (09 2009)"},{"issue":"5","key":"29_CR13","doi-asserted-by":"publisher","first-page":"649","DOI":"10.1109\/TSE.2010.62","volume":"37","author":"Y Jia","year":"2011","unstructured":"Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Trans. Softw. Eng. 37(5), 649\u2013678 (2011). https:\/\/doi.org\/10.1109\/TSE.2010.62","journal-title":"IEEE Trans. Softw. Eng."},{"key":"29_CR14","unstructured":"Klocwork. https:\/\/www.perforce.com\/products\/klocwork. Accessed 18 May 2022"},{"key":"29_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03809-3","volume-title":"Introduction to Formal Hardware Verification","author":"T Kropf","year":"1999","unstructured":"Kropf, T.: Introduction to Formal Hardware Verification, 1st edn. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/978-3-662-03809-3","edition":"1"},{"key":"29_CR16","unstructured":"Landelijke Tunnelstandaard (National Tunnel Standard). http:\/\/publicaties.minienm.nl\/documenten\/landelijke-tunnelstandaard. Accessed Apr 2022"},{"key":"29_CR17","doi-asserted-by":"crossref","unstructured":"Matsakis, N.D., Klock II, F.S.: The rust language. In: ACM SIGAda Ada Letters, vol. 34, pp. 103\u2013104. ACM (2014)","DOI":"10.1145\/2692956.2663188"},{"key":"29_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/978-3-030-34968-4_23","volume-title":"Integrated Formal Methods","author":"W Oortwijn","year":"2019","unstructured":"Oortwijn, W., Huisman, M.: Formal verification of an industrial safety-critical traffic tunnel control system. In: Ahrendt, W., Tapia Tarifa, S.L. (eds.) IFM 2019. LNCS, vol. 11918, pp. 418\u2013436. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-34968-4_23"},{"key":"29_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-030-45190-5_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"W Oortwijn","year":"2020","unstructured":"Oortwijn, W., Huisman, M., Joosten, S.J.C., van de Pol, J.: Automated verification of parallel nested DFS. In: Biere, A., Parker, D. (eds.) TACAS 2020. LNCS, vol. 12078, pp. 247\u2013265. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_14"},{"key":"29_CR20","unstructured":"Rubbens, R.: Improving Support for Java Exceptions and Inheritance in VerCors, May 2020. http:\/\/essay.utwente.nl\/81338\/"},{"key":"29_CR21","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2022.02.027","author":"M Safari","year":"2022","unstructured":"Safari, M., Huisman, M.: Formal verification of parallel prefix sum and stream compaction algorithms in CUDA. Theoret. Comput. Sci. (2022). https:\/\/doi.org\/10.1016\/j.tcs.2022.02.027","journal-title":"Theoret. Comput. Sci."},{"key":"29_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-030-55754-6_10","volume-title":"NASA Formal Methods","author":"M Safari","year":"2020","unstructured":"Safari, M., Oortwijn, W., Joosten, S., Huisman, M.: Formal verification of parallel prefix sum. In: Lee, R., Jha, S., Mavridou, A., Giannakopoulou, D. (eds.) NFM 2020. LNCS, vol. 12229, pp. 170\u2013186. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-55754-6_10"},{"key":"29_CR23","unstructured":"\u015eakar, O.: Extending support for Axiomatic Data Types in VerCors, April 2020. https:\/\/essay.utwente.nl\/80892\/"},{"key":"29_CR24","unstructured":"Sonarqube. https:\/\/www.sonarqube.org\/. Accessed 18 May 2022"},{"key":"29_CR25","unstructured":"Technolution. https:\/\/www.technolution.eu. Accessed Apr 2022"},{"key":"29_CR26","doi-asserted-by":"publisher","unstructured":"Timmer, M., Brinksma, H., Stoelinga, M.: Model-based testing, NATO science for peace and security series D: Information and Communication Security, vol. 30, pp. 1\u201332. IOS Press (2011). https:\/\/doi.org\/10.3233\/978-1-60750-711-6-1","DOI":"10.3233\/978-1-60750-711-6-1"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-19849-6_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,20]],"date-time":"2022-10-20T00:11:54Z","timestamp":1666224714000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-19849-6_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031198489","9783031198496"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-19849-6_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"17 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}