Formal Development and Verification of a Distribut

FormalDevelopmentandVericationofaDistributedRailwayControlSystemAnneE.Haxthausen1andJanPeleska21Dept.ofInformationTechnology,Techn.UniversityofDenmark,DK-2800Lyngby,[e-mail]2BISS,UniversitatBremen,P.O.Box330440,D-28334Bremen,[e-mail]theconceptforadistributedrail-waycontrolsystemandpresentthespecicationandvericationofthemainalgorithmusedforsafedistributedcontrol.Ourdesignandveri-cationapproachisbasedontheRAISEmethod,startingwithhighlyab-stractalgebraicspecicationswhicharetransformedintodirectlyimple-mentabledistributedcontrolprocessesbyapplyingaseriesofrenementandvericationsteps.Concretesafetyrequirementsarederivedfromanabstractversionthatcanbeeasilyvalidatedwithrespecttosoundnessandcompleteness.Complexityisfurtherreducedbyseparatingthesys-temmodelintoadomainmodeldescribingthephysicalsysteminabsenceofcontrolandacontrollermodelintroducingthesafety-relatedcontrolmechanismsasaseparateentitymonitoringobservablesofthephysicalsystemtodecidewhetheritissafeforatraintomoveorforapointtobeswitched.1IntroductionThepresentmodernisationofEuropeanrailwaynetworksraisesalargevarietyofissuesrelatedtothedesignandvericationofrailwaycontrolsystems.Oneoftheseproblemsisthequestionhowtodesigncontrolsystemsforsmalllocalnetworksthatcanonlyoperateeectivelyifthecostsforinitialinstallation,operationandmaintenanceofthecontrolsystemarelow.Today’scentralisedinterlockingsystems{atleastthosewhichareavailableinGermany{arefartooexpensiveforsuchsmall(possiblyprivatised)networks.Apromisingapproachistodistributethetasksoftraincontrol,trainprotectionandinterlockingoveranetworkofcooperatingcomponentsusingthestandardcommunicationfacilitiesoeredbymobiletelephoneproviders.Ontheotherhand,adistributedcontrolconceptalsointroducesnewsafetyissuesthatcouldbedisregardedaslongascentralisedcontrolwasapplied:First,thenewcommunicationmediumrequiressecurityandreliabilitymechanismsthatwereunnecessaryforcentralisedsystemstransmittingcontrolcommandstosignalsandpointsoverwires.Second,thedistributionofacontrolalgorithmoverseveralcomponentsraisesnewdesignandvericationissues,sincetheconceptofaglobalstatespaceasavailableinacentralisedinterlockingsystemcannolongerbeimplemented.Inthisarticle,wewilldescribetheconceptofadistributedrailwaycontrolsystemconsistingofswitchboxes(SB),eachonelocallycontrollingapoint,andtraincontrolcomputers(TCC)residinginthetrainenginesandcollectingthelocalstateinformationfromswitchboxesalongthetracktoderivethedecisionwhetherthetrainmayenterthenexttracksegment.Thesystemconceptdoesnotrequiresignalsalongthetrack,sincethe\go/no-godecisionsareperformedandindicatedinthetraincontrolcomputers.Wegiveanoverviewoverthefor-malspecicationandvericationofthemaincontrolalgorithmexecutedbythedistributedcooperatingcontrolcomponents.Thesystemisdesignedtooperateonsimplenetworks,whichmeansinourcontextthattherearetwodistinguisheddestinationsAandB,suchthatateachtracksegmentofthenetworkthereisauniquelydeneddirectiontoreachAandB,respectively.Typically,thisdeni-tionappliestonetworkswhicharenothighlyfrequentedbytrainsandconnecttwomainstationswithsmallintermediatestations(Figure1).ABdirectionABdirectionBAFig.1.Simplerailwaynetwork.OurspecicationandvericationapproachisbasedontheRAISEformalmethodandtoolset[Rlg92,Rmg95]andfollowstheinvent-and-verifyparadigm.Toaddresssafetyissuesinasystematicwaythestandardprocedure(see[Sto96])separatingtheequipmentundercontrol{thatis,therailwaynetworkwithitstrains{fromthecontrolsystem{inourcase,thesetofTCCsandSBs{isapplied.Tothisend,werstdevelopabstractalgebraicspecicationsforthedomainmodel,i.e.,therailwaynetworkandthetrainstobecontrolled,andthesafetyrequirementsstatingthatthesystemmustnotperformatransitionintoahazardousstatewheretrainsmaycollideorderailingmightoccur.Theserequire-mentsareexpressedasconditionsabouttheobservablesofthedomainmodel.Usingstepwiserenementandaccompanyingvericationsteps,weintroduceadditionalobservablesthatmaybemonitoredbyacontrollergivingthe\canmove/cannotmoveconditionsforeachtrainandthe\canbeswitched/cannotbeswitchedconditionsforeachpoint.Thecompletenessandconsistencyoftheseconditionsisveriedbyprovingrenementrelationstothehigher-levelspecicationswhichalreadyhavebeenprovedtobeconsistentwiththeinitialsafetyrequirements.Therststageoftheinvent-and-verifydevelopmentendswhentheobservablesofthelastrenementneededtocontrolthesafetyoftrainmovementsandpointswitchingareimplementableinthesensethattheycan2betransformedintoaconcretestatespacethatmaybeconvenientlypartitionedamongasetofdistributedcooperatingprocesses.Thesecondstagespeciesandveriestheconcrete{i.e.,implementable{distributedcontrollermodelbyintroducingcommunicatingprocesseswhichrepresenttraincontrolcomput-ersandswitchboxes.TheTCCprocessescollectstateinformationfromtheSBprocessestomakethe\canmove/cannotmovedecisions.TheSBprocessesstoretherelevantstateinformationtotakethe\canbeswitched/cannotbeswitcheddecisionsfortheirlocalpoints.Theresultingcontrollerisanondeter-ministicdistribu