Extraction of Critical Scenarios in a Railway Leve

InternationalJournalofComputers,Communications&ControlVol.II(2007),No.3,pp.252-268ExtractionofCriticalScenariosinaRailwayLevelCrossingControlSystemMalikaMedjoudj,PascalYimAbstract:Thispaperdealswiththesafetyofthelevelcrossingcontrolsystem.WeproposeonewayofthesafetyevaluationwitchconsistontheextractionoffearedscenariosinthePetrinetmodelofthesystem.WeuseESA_PetriNettool(ExtractionScenarios&AnalyzerbyPetriNetmodel)thatwasdevelopedintheaimofextractionoffearedscenariosincomputer-controlledsystems.Thesescenarioscharacterizethesequencesofactionsleadingtodangeroussituations.Thetakingintoaccountofthefailures,thetemporalconstraintsandpartiallythecontinuousdynamic(bytemporalabstraction)ofthesystemmakesitpossibletorespecttheorderofappearanceoftheeventsinthegeneratedscenarios.Keywords:Criticalscenarios,hybriddynamic,levelcrossingcontrolsystem,safety,temporalPetrinet1IntroductionOnewaytoevaluatethesafety[2]ofcomplexsystemsuchasalevelcrossingcontrolsystem(lccs)istheextractionofcriticalscenariosleadingtothefearedstates.Aqualitativeanalysismethodofsafety,aimingtheextractionofallthecriticalscenariosfromaPetriNetmodel[5]ofcomputer-controlledsystemswasdevelopedby[3].Thisapproachwitchisanextensionofamethoddevelopedby[6]butwhichoperatedonlyonthediscreteaspectofthesystem,takesintoaccountthecontinuousaspectofthesystemandthetemporalspecifications.Thisapproachbasedonlinearlogic[7]determinesmorepreciselytheexactconditionsoftheoccurrenceofthefearedevent,i.ewhathasledthesystemtoleaveitsnormaloperationandtoevolveintothefearedstate.Theoriginalityofthisapproachisthattheorderofoccurrenceoftheeventsistakenintoaccount,andimpossiblescenarioswithrespecttocontinuousdynamicsandtemporalspecificationsofthesystemareeliminated.TheautomationofallstagesoftheprocesshasledtothedevelopmentofESA_PetriNettool(Extraction&ScenariosAnalyserbyPetriNetmodel)[4]thathasbeeninterfacedwithTINAtool(TimePetriNetAnalyzer)[8].WewilluseinthispaperESA_PetriNettooltoextractdangerousscenariosfromthelevelcrossingbenchmarkpublishedby[10].Wewillpresentthemethodofextractionoffearedscenariosandthebasicofthealgorithminsec-tion2,thelevelcrossingcontrolsysteminsection3,itsPetriNetmodellinginsection4,theuseofESA_PetriNettooltogeneratethecriticalscenariosinthesection5andwewillendbyaconclusion.2MethodofextractionoffearedscenariosTheapplicationofthismethodrequiresthemodellingofthesystembyatimePetriNetmodelandidentifyingtheplacesofnominalbehaviour.TheappropriatePetrinetmodellingofcomputer-controlledsystemsisaPredicateTransitionsDifferentialStochasticPetrinet(PTDSPetrinet)astheyaregenerallyhybrid(discreteandcontinuousdynamics)andtheresafetyanalysisrequiretakingintoaccountfailures.AtemporalabstractionisnecessarytotranslatethismodeltoatimePetrinetbyassociatingtothetransitionsatemporalintervaloffiringcorrespondingtothetimewhichthesystemcanspendtoreachthestateinquestion.Apreliminaryanalysiswillrefinefieldsofvariablesaccordingtovariousaccessiblemarkingsbyreasoningontheinvariantsofplaces.Indeed,theinvariantsofplacesdeterminethepossibledynamics,andwhichotherplacescanbesimultaneouslymarkedwhenatokenispresentinagivenplace.Copyright©2006-2007byCCCPublicationsExtractionofCriticalScenariosinaRailwayLevelCrossingControlSystem2532.1PrincipalThemethodofextractionoffearedscenariosismadeupoftwosteps[3]:abackwardreasoningandaforwardreasoning.ThebackwardreasoningtakesasaninitialmarkinginthereversedPetrinetmodel(theinitialPetrinetinwhichallthearcsarereversed),theonlytargetstate(feared)andseeksexhaustivelyallthescenariosmakingitpossibletoconsumetheinitialmarking(fearedstatesinceforwardreasoning)andreachafinalmarkingcomposedonlyofplacesassociatedtothenormaloperation.TheforwardreasoningtakesasaninitialstatetheseplacesofnormaloperationintheinitialPetrinetmodel.Theobjectiveistolocatethejunctionsbetweenthefearedbehaviourandthenormaloperationofthesystemaswellastheconditionsimpliedinthesejunctions.Thuswehavenotonlytheexplanationofthedangerousbehaviourbutalsoofstrategiesallowingitsavoidance.Asignificantpointofthemethodisthatthecontextinwhichoccurredthefearedeventisenrichedgradually.Theenrichment(ofmarking)consistsonputtingtokensinemptyplacesinthePetrinetmodelwhenitisnecessarytomakeevolvethesystemandgeneratescenarios.Theinvariantofplacesareusedasamechanismofcheckingthecoherenceoftheenrichmentofmarking.Indeedthenewtokensaddedareremovediftheydonotrespectthedynamicsofthesystem.Eachscenarioisgiveninformofapartialorderbetweentheeventsnecessarytotheappearanceofthefearedeventwhatdiffersfromafailuretree,whichgivesawholeofstaticcombinationsofthepartialstatesnecessaryforobtainingthefearedstate.2.2DealingwithcontinuousdynamicsbytemporalabstractionThismethodtakesintoaccounttheconditionsassociatedtothefiringofcertaintransitions.Theseconditionsarethresholdsinvolvingcontinuousvariables.Bytemporalapproximationofthehybriddy-namics,thesethresholdsaretransformedtodurations,whichcorrespondtotimethatthesystemputstoreachwhenthetransitionsareenabled.Fromaqualitativepointofview,theobjectiveistodeterminethefiringorderofthetransition.Thus,whenweenric