Studies in Systems, Decision and Control 458 Muhammad Atif Jan Friso Groote Understanding Behaviour of Distributed Systems Using mCRL2 Studies in Systems, Decision and Control Volume 458 SeriesEditor JanuszKacprzyk,SystemsResearchInstitute,PolishAcademyofSciences, Warsaw,Poland The series “Studies in Systems, Decision and Control” (SSDC) covers both new developments and advances, as well as the state of the art, in the various areas of broadly perceived systems, decision making and control–quickly, up to date and withahighquality.Theintentistocoverthetheory,applications,andperspectives onthestateoftheartandfuturedevelopmentsrelevanttosystems,decisionmaking, control, complex processes and related areas, as embedded in the fields of engi- neering, computer science, physics, economics, social and life sciences, as well as the paradigms and methodologies behind them. The series contains mono- graphs,textbooks,lecturenotesandeditedvolumesinsystems,decisionmakingand controlspanningtheareasofCyber-PhysicalSystems,AutonomousSystems,Sensor Networks, Control Systems, Energy Systems, Automotive Systems, Biological Systems, Vehicular Networking and Connected Vehicles, Aerospace Systems, Automation, Manufacturing, Smart Grids, Nonlinear Systems, Power Systems, Robotics,SocialSystems,EconomicSystemsandother.Ofparticularvaluetoboth thecontributorsandthereadershiparetheshortpublicationtimeframeandtheworld- widedistributionandexposurewhichenablebothawideandrapiddisseminationof researchoutput. IndexedbySCOPUS,DBLP,WTIFrankfurteG,zbMATH,SCImago. AllbookspublishedintheseriesaresubmittedforconsiderationinWebofScience. · Muhammad Atif Jan Friso Groote Understanding Behaviour of Distributed Systems Using mCRL2 MuhammadAtif JanFrisoGroote DepartmentofComputerScience DepartmentofMathematicsandComputer andInformationTechnology Science TheUniversityofLahore EindhovenUniversityofTechnology Lahore,Pakistan Eindhoven,Noord-Brabant TheNetherlands ISSN 2198-4182 ISSN 2198-4190 (electronic) StudiesinSystems,DecisionandControl ISBN 978-3-031-23007-3 ISBN 978-3-031-23008-0 (eBook) https://doi.org/10.1007/978-3-031-23008-0 ©TheEditor(s)(ifapplicable)andTheAuthor(s),underexclusivelicensetoSpringerNature SwitzerlandAG2023 Thisworkissubjecttocopyright.AllrightsaresolelyandexclusivelylicensedbythePublisher,whether thewholeorpartofthematerialisconcerned,specificallytherightsoftranslation,reprinting,reuse ofillustrations,recitation,broadcasting,reproductiononmicrofilmsorinanyotherphysicalway,and transmissionorinformationstorageandretrieval,electronicadaptation,computersoftware,orbysimilar ordissimilarmethodologynowknownorhereafterdeveloped. Theuseofgeneraldescriptivenames,registerednames,trademarks,servicemarks,etc.inthispublication doesnotimply,evenintheabsenceofaspecificstatement,thatsuchnamesareexemptfromtherelevant protectivelawsandregulationsandthereforefreeforgeneraluse. Thepublisher,theauthors,andtheeditorsaresafetoassumethattheadviceandinformationinthisbook arebelievedtobetrueandaccurateatthedateofpublication.Neitherthepublishernortheauthorsor theeditorsgiveawarranty,expressedorimplied,withrespecttothematerialcontainedhereinorforany errorsoromissionsthatmayhavebeenmade.Thepublisherremainsneutralwithregardtojurisdictional claimsinpublishedmapsandinstitutionalaffiliations. ThisSpringerimprintispublishedbytheregisteredcompanySpringerNatureSwitzerlandAG Theregisteredcompanyaddressis:Gewerbestrasse11,6330Cham,Switzerland Dedicatedtoourfamilies Preface Understandingadistributedsystem’sbehaviourmeansgettinginsightintowhether the system meets its expectations. Giving such a surety is challenging, primarily whenasystemconsistsofmultipleparticipants.Theseparticipantscaninteractwith eachotherinfarmorewaysthanwecanimagine. Inthisbook,weexplainhowtomodelthebehaviourofcommunicatingsystems andgenerate,reduceandvisualiseitasalabelledtransitionsystem.Wealsoshow howtodomodel-checking,whichallowscheckingpropertiesonthebehaviour,such aswhetherthebehaviourisfreeofdeadlocks.Nevertheless,asweusethemodalmu- calculus with data, virtually any conceivable safety, liveness and fairness property canbeformulatedandchecked. Applyingmodel-checkingmakeseveryone’seyebrowhighastheresultsareoften surprising.Usingcounter-examplescanrevealbehaviourindistributedsystemsthat noone,includingthedevelopers,deemedpossible,andassuch,itisaninvaluable tooltoobtainessentialinsightintothebehaviourofmodernprogrammedsystems. It is a general perception that model-checking has a steep learning curve. In this book, we try to mitigate this by introducing all concepts with small exam- plesand thoroughly explaining systemspecifications lineby line.WeusemCRL2 (microCommonRepresentationLanguage2)andthemodalmu-calculus,whichare specialisedlanguagesthatspecifyadistributedsystemandformulatesystemprop- erties.Theselanguagescomewithaneffectivetoolset,whichisopensourceandcan befreelyused(www.mcrl2.org). This book is introductory and comprises subjects from installing the toolset mCRL2toanalysingsimplesystems.Westartwithwritinghelloworldtypesystems andgraduallyincreasethecomplexityofexamplesandexercises.So,anyonehaving someknowledgeofcomputerprogramming,logicandbasicmathematicscanstudy thisbookandwilllearnhowtomodel-checkcommunicationprotocols,distributed algorithmsandinteractingsystems.Wefocustoexplaineverytopicwithsufficient vii viii Preface examples and exercises. A chapter on modelling and solving puzzles and another chapteronhowtomodelheartbeatprotocolsillustratethetechniques. Lahore,Pakistan MuhammadAtif Eindhoven,TheNetherlands JanFrisoGroote February2023 Acknowledgments We acknowledge the contribution of many people who gave their feedback and support.ShaziaHussain(wifeofMuhammadAtif)keptaskingabouttheprogress of the book and Paula Versteegen (wife of Jan Friso Groote) kept listening to an infinitestreamofunsolicitedexplanationsaboutsystembehaviour.Weappreciatethe guidanceofDr.AliKhan,AssociateEditorofSpringer,whosuggestedpublishingthis bookwithSpringerNatureBookServices.Mr.PrasannaKumar,alsofromSpringer, kindlypushedustocompletethisbookbysendingemailsfromtimetotime. We thank Ir. Olav Bunte (Ph.D. student at TU/e Netherlands) and Dr.ir. Jeroen Keiren (Assistant Professor at TU/e, Netherlands) for answering every question aboutthetoolsetmCRL2.ThanksalsogotoDr.ir.WiegerWesselinkandIr.Maurice Laveaux,aswellasmanyothers,formaintaininganddevelopingthemCRL2toolset. WearealsothankfultoDr.IjazAhmedandMr.ImranShafi,whogavetheirvaluable feedback. OfficialsfromtheUniversityofLahorewhoalwaysremained amotiva- tion are Mr. Awais Raoof (chairman), Prof. Dr. Mujahid Kamran (former rector) andProf.Dr.MuhammadAshraf(rector).Lastly,wewouldliketoacknowledgethe constant support of Bakhtawar Atif, Fatima Atif, Muhammad Hassan Chattha and MuhammadAtharChattha. Lahore,Pakistan MuhammadAtif Eindhoven,TheNetherlands JanFrisoGroote February2023 ix Introduction Welcome Welcometothefirsteditionofthebook.Thisbookintendstocreateaninterestto reasonaboutthecorrectnessofthebehaviourofprogrammedsystems.Therearea lotofsuchsystemsaroundusandavailableintheliteraturethatneedstobestudied andcorrected.Forexample,wecanstudytheprotocolofanATM(automatedteller machine),e-Tagsystemforroadtaxcollection,e-Commercesystemsorothersystems having communicating processes. It can be surprising to know that many of the existingdistributedalgorithmsusedinsuchsystemsarenotcompletelycorrect,which can effectively be found by formal verification. In model-checking, the complete behaviourofasystemismodelledandthensearchedexhaustively. WhoIsThisBookFor? ThisbookisforthosewhowanttousemCRL2forautomaticallyanalysingsystem behaviour.Thetargetedsystemsforsuchananalysisarethosesystemshavingconcur- rent processes with inter-process communication. In this book, we study system modellingandmodel-checkingtechniques.Interestingly,model-checkingprovides beneficialresults,butatthesametime,itposesparticularchallengesaswell.Formu- latingbehaviourprecisely,especiallyformalisingpropertiesthatthebehaviourmust have,isnotalwayseasy.Notonlyitishardtounderstandthebehaviourandrequire- ments,oftengiveninambiguousnaturallanguage,butcorrectlyencodingthemusing minimalormaximalfixedpointmodalitiesrequiressometrainingandexperience. Besidesthat,amodelledsystemmaybecomesocomplexthatthetoolscannolonger analyseit.Thisphenomenonisoftenreferredtoasthestatespaceexplosionproblem. In this book, we study these challenges and the methods to address those challengesinordertoapplymodel-checkingeffectively. xi