Tiziana Margaria · Bernhard Steffen (Eds.) Leveraging Applications of Formal Methods, 8 7 4 2 Verification and Validation 1 S C N Applications L 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 12478 Founding Editors Gerhard Goos Karlsruhe Institute of Technology, Karlsruhe, Germany Juris Hartmanis Cornell University, Ithaca, NY, USA Editorial Board Members Elisa Bertino Purdue University, West Lafayette, IN, USA Wen Gao Peking University, Beijing, China Bernhard Steffen TU Dortmund University, Dortmund, Germany Gerhard Woeginger RWTH Aachen, Aachen, Germany Moti Yung Columbia University, New York, NY, USA More information about this series at http://www.springer.com/series/7407 Tiziana Margaria Bernhard Steffen (Eds.) (cid:129) Leveraging Applications of Formal Methods, fi Veri cation and Validation Applications 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020 – Rhodes, Greece, October 20 30, 2020 Proceedings, Part III 123 Editors Tiziana Margaria Bernhard Steffen University of Limerick andLero TU Dortmund Limerick, Ireland Dortmund, Germany ISSN 0302-9743 ISSN 1611-3349 (electronic) Lecture Notesin Computer Science ISBN 978-3-030-61466-9 ISBN978-3-030-61467-6 (eBook) https://doi.org/10.1007/978-3-030-61467-6 LNCSSublibrary:SL1–TheoreticalComputerScienceandGeneralIssues ©SpringerNatureSwitzerlandAG2020 Thisworkissubjecttocopyright.AllrightsarereservedbythePublisher,whetherthewholeorpartofthe material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting, reproduction on microfilms or in any other physical way, and transmission or information storageandretrieval,electronicadaptation,computersoftware,orbysimilarordissimilarmethodologynow knownorhereafterdeveloped. Theuseofgeneraldescriptivenames,registerednames,trademarks,servicemarks,etc.inthispublication doesnotimply,evenintheabsenceofaspecificstatement,thatsuchnamesareexemptfromtherelevant protectivelawsandregulationsandthereforefreeforgeneraluse. Thepublisher,theauthorsandtheeditorsaresafetoassumethattheadviceandinformationinthisbookare believedtobetrueandaccurateatthedateofpublication.Neitherthepublishernortheauthorsortheeditors give a warranty, expressed or implied, with respect to the material contained herein or for any errors or omissionsthatmayhavebeenmade.Thepublisherremainsneutralwithregardtojurisdictionalclaimsin publishedmapsandinstitutionalaffiliations. ThisSpringerimprintispublishedbytheregisteredcompanySpringerNatureSwitzerlandAG Theregisteredcompanyaddressis:Gewerbestrasse11,6330Cham,Switzerland Introduction It is our responsibility, as general and program chairs, to welcome the participants to the 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), planned to take place in Rhodes, Greece, during October 20–30, 2020, endorsedby theEuropean Association ofSoftware Science and Technology (EASST). This year’s event follows the tradition of its symposia forerunners held in Paphos, Cyprus (2004 and 2006), Chalkidiki, Greece (2008), Crete, Greece (2010 and 2012), Corfu,Greece(2014and2016),andmostrecentlyinLimassol,Cyprus(2018),andthe series of ISoLA workshops in Greenbelt, USA (2005), Poitiers, France (2007), Potsdam, Germany (2009), Vienna, Austria (2011), and Palo Alto, USA (2013). Considering that this year’s situation is unique and unlike any previous one due to theongoingCOVID-19pandemic,andthatISoLA’ssymposiumtouchandfeelismuch unlike most conventional, paper-based conferences, after much soul searching we are faced with a true dilemma. “Virtualizing” the event, as many conferences have done, violates the true spirit of the symposium, which is rooted in the gathering of com- munitiesandthediscussionswithinandacrossthevariouscommunitiesmaterializedin thespecialtracksandsatelliteevents.Keepingwiththephysicalmeetingandholdingit in a reduced form (as many may not be able to or feel comfortable with travel) under strictsocialdistancingrulesmayalsoendupnotbeingfeasible.Atthetimeofwriting there is a resurgence of cases in several countries, many nations are compiling “green lists” of countries with which they entertain free travel relations, and these lists are updated–mostfrequentlyshortened–atshortnotice,withsevereconsequenceforthe travelers. Many governments and universities are again strengthening the travel restrictions for their employees, and many of us would anyway apply caution due to our own specific individual situation. Tobeabletoreactasflexiblyaspossibletothissituation,wedecidedtosplitISoLA 2020 into two parts, one this year and one in October 2021, with the track organizers decidingwhentheirtrackwilltakeplace.Sofarbothdateshavepromoters,butitmay still happen that, in the end, the entire event needs to move. All accepted papers are published in time, but some tracks will present their papers at the 2021 event. Asinthepreviouseditions,ISoLA2020providesaforumfordevelopers,users,and researchers to discuss issues related to the adoption and use of rigorous tools and methodsforthespecification,analysis,verification,certification,construction,test,and maintenance of systems from the point of view of their different application domains. Thus, since 2004, the ISoLA series of events serves the purpose of bridging the gap between designers and developers of rigorous tools on one side, and users in engi- neering and in other disciplines on the other side. It fosters and exploits synergetic relationships among scientists, engineers, software developers, decision makers, and other critical thinkers in companies and organizations. By providing a specific, dialogue-oriented venue for the discussion of common problems, requirements, vi Introduction algorithms, methodologies, and practices, ISoLA aims in particular at supporting researchers in their quest to improve the usefulness, reliability, flexibility, and effi- ciencyoftoolsforbuildingsystems,andusersintheirsearchforadequatesolutionsto their problems. Theprogramofthesymposiumconsistsofacollection ofspecial tracksdevotedto the following hot and emerging topics: (cid:129) Reliable Smart Contracts: State-of-the-art, Applications, Challenges and Future Directions (Organizers: Gordon Pace, César Sànchez, Gerardo Schneider) (cid:129) Engineering of Digital Twins for Cyber-Physical Systems (Organizers: John Fitzgerald, Pieter Gorm Larsen, Tiziana Margaria, Jim Woodcock) (cid:129) Verification and Validation of Concurrent and Distributed Systems (Organizers: Cristina Seceleanu, Marieke Huisman) (cid:129) Modularity and (De-)composition in Verification (Organizers: Reiner Hähnle, Eduard Kamburjan, Dilian Gurov) (cid:129) Software Verification Tools (Organizers: Markus Schordan, Dirk Beyer, Irena Boyanova) (cid:129) X-by-Construction: Correctness meets Probability (Organizers: Maurice H. ter Beek, Loek Cleophas, Axel Legay, Ina Schaefer, Bruce W. Watson) (cid:129) Rigorous Engineering of Collective Adaptive Systems (Organizers: Rocco De Nicola, Stefan Jähnichen, Martin Wirsing) (cid:129) Automated Verification of Embedded Control Software (Organizers: Dilian Gurov, Paula Herber, Ina Schaefer) (cid:129) Automating Software Re-Engineering (Organizers: Serge Demeyer, Reiner Hähnle, Heiko Mantel) (cid:129) 30 years of Statistical Model Checking! (Organizers: Kim G. Larsen, Axel Legay) (cid:129) From Verification to Explanation (Organizers: Holger Herrmanns, Christel Baier) (cid:129) Formal methods for DIStributed COmputing in future RAILway systems (DisCo- Rail 2020) (Organizers: Alessandro Fantechi, Stefania Gnesi, Anne Haxthausen) (cid:129) Programming: What is Next? (Organizers: Klaus Havelund, Bernhard Steffen) With the embedded events: (cid:129) RERS: Challenge on Rigorous Examination of Reactive Systems (Falk Howar, Markus Schordan, Bernhard Steffen) (cid:129) Doctoral Symposium and Poster Session (A. L. Lamprecht) (cid:129) Industrial Day (Falk Howar, Johannes Neubauer, Andreas Rausch) Introduction vii Colocated with the ISoLA symposium is: (cid:129) STRESS 2020 – 5th International School on Tool-based Rigorous Engineering of Software Systems (J. Hatcliff, T. Margaria, Robby, B. Steffen) Altogether the ISoLA 2020 proceedings comprises four volumes, Part 1: Verifica- tionPrinciples,Part2:EngineeringPrinciples,Part 3:Applications, andPart4:Tools, Trends, and Tutorials, which also covers the associated events. We thank the track organizers, the members of the Program Committee and their referees for their effort in selecting the papers to be presented, the local organization chair, Petros Stratis, and the EasyConferences team for their continuous and precious supportduringtheentiretwo-yearperiodprecedingtheevents,andSpringerforbeing, asusual,averyreliablepartnerfortheproceedingsproduction.Finally,wearegrateful to Kyriakos Georgiades for his continuous support for the website and the program, and to Markus Frohme and Julia Rehder for their help with the editorial system Equinocs. Specialthanksareduetothefollowingorganizationfortheirendorsement:EASST (European Association of Software Science and Technology) and Lero – The Irish SoftwareResearchCentre,andourowninstitutions–TUDortmundUniversityandthe University of Limerick. We wish you, as an ISoLA participant, a wonderful experience at this edition, and for you, reading the proceedings at a later occasion, valuable new insights that hope- fully contribute to your research and its uptake. August 2020 Tiziana Margaria Bernhard Steffen Organization Symposium Chair Tiziana Margaria University of Limerick and Lero, Ireland PC Chair Bernhard Steffen TU Dortmund University, Germany PC Members Christel Baier Technische Universität Dresden, Germany Maurice ter Beek ISTI-CNR, Italy Dirk Beyer LMU Munich, Germany Irena Bojanova NIST, USA Loek Cleophas EindhovenUniversityofTechnology,TheNetherlands Rocco De Nicola IMT Lucca, Italy Serge Demeyer Universiteit Antwerpen, Belgium Alessandro Fantechi University of Florence, Italy John Fitzgerald Newcastle University, UK Stefania Gnesi CNR, Italy Kim Guldstrand Larsen Aalborg University, Denmark Dilian Gurov KTH Royal Institute of Technology, Sweden John Hatcliff Kansas State University, USA Klaus Havelund Jet Propulsion Laboratory, USA Anne E. Haxthausen Technical University of Denmark, Denmark Paula Herber University of Münster, Germany Holger Hermanns Saarland University, Germany Falk Howar Dortmund University of Technology and Fraunhofer ISST, Germany Marieke Huisman University of Twente, The Netherlands Reiner Hähnle Technische Universität Darmstadt, Germany Stefan Jähnichen TU Berlin, Germany Eduard Kamburjan Technische Universität Darmstadt, Germany Anna-Lena Lamprecht Utrecht University, The Netherlands Peter Gorm Larsen Aarhus University, Denmark Axel Legay Université Catholique de Louvain, Belgium Heiko Mantel Technische Universität Darmstadt, Germany Tiziana Margaria University of Limerick and Lero, Ireland Johannes Neubauer Materna, Germany Gordon Pace University of Malta, Malta Cesar Sanchez IMDEA Software Institute, Madrid, Spain x Organization Ina Schaefer TU Braunschweig, Germany Gerardo Schneider University of Gothenburg, Sweden Markus Schordan Lawrence Livermore National Laboratory, USA Cristina Seceleanu Mälardalen University, Sweden Bernhard Steffen TU Dortmund University, Germany Bruce Watson Stellenbosch University, South Africa Martin Wirsing Ludwig-Maximilians-Universität München, Germany James Woodcock University of York, UK Reviewers Aho, Pekka Hungar, Hardi Aichernig, Bernhard Inverso, Omar Backeman, Peter Iosti, Simon Baranov, Eduard Jacobs, Bart Basile, Davide Jaeger, Manfred Beckert, Bernhard Jensen, Peter Bensalem, Saddek Johnsen, Einar Broch Bettini, Lorenzo Jongmans, Sung-Shik Beyer, Dirk Jähnichen, Stefan Bourr, Khalid Kanav, Sudeep Bubel, Richard Konnov, Igor Bures, Tomas Kosak, Oliver Casadei, Roberto Kosmatov, Nikolai Castiglioni, Valentina Kretinsky, Jan Ciatto, Giovanni Könighofer, Bettina Cimatti, Alessandro Lanese, Ivan Damiani, Ferruccio Lecomte, Thierry Di Marzo Serugendo, Giovanna Lluch Lafuente, Alberto Duong, Tan Loreti, Michele Filliâtre, Jean-Christophe Maggi, Alessandro Fränzle, Martin Mariani, Stefano Gabor, Thomas Mazzanti, Franco Gadducci, Fabio Morichetta, Andrea Galletta, Letterio Nyberg, Mattias Geisler, Signe Omicini, Andrea Gerostathopoulos, Ilias Orlov, Dmitry Guanciale, Roberto Pacovsky, Jan Heinrich, Robert Parsai, Ali Hillston, Jane Peled, Doron Hnetynka, Petr Piho, Paul Hoffmann, Alwin Pugliese, Rosario