Analysis and Verification Challenges Cyber-Physical Transportation Systems

混合系统建模与验证

AnalysisandVeri cationChallengesfor

Cyber-PhysicalTransportationSystems

EdmundM.Clarke1,BruceKrogh2,Andr´ePlatzer1,andRajRajkumar2

2ComputerScienceDepartment,CarnegieMellonUniversity,Pittsburgh,PAElectrical&ComputerEngineeringDepartment,CarnegieMellonUniversity,Pittsburgh,PA

{emc|krogh|aplatzer|raj}@cmu.edu1

Abstract.Substantialtechnologicalandengineeringadvancesinvariousdisciplinesmakeitpossiblemorethaneverbeforetoprovideautonomouscontrolchoicesforcars,trains,andaircraft.Correctautomaticcontrolcanimproveoverallsafetytremendously.Yet,ensuringasafeoperationofthosecontrolassistantsunderallcircumstancesrequiresanalysistechniquesthatarepreparedfortherisingcomplexityresultingfromcombinationsofseveralcomputerizedsafetymeasures.Weidentifycaseswherecyber-physicaltransportationsystemsposeparticularlydemandingchallengesforfutureresearchinformalanalysistechniques.

1Cyber-PhysicalTransportationSystems

Cyber-physicalsystemsarebecomingmoreimportantinthesupervisoryandsafetycontrolfunctionsofrail-based,airborne,andautomotivetransportationsystemsthathavetypicallybeenperformedbyhumanoperatorsbefore.Improvementsinsensoraccuracy,computationalresources,andtheirunderstandingenablemanufacturerstoassistdriversandpilotsonalevelofsophisticationthathasneverbeenpossiblebefore.Transportationassistancetechnologyhasmostimpactwhensupportingsafety-criticaldriverorpilotdecisionstopreventfatalaccidents.Itisofultimateimportancethatthesesafety-criticalcontroldecisionsarecorrect.Controlassistancetechnologycanin uencetheactualcontrolchoicesthattakee ectinthetransportationsysteminseveralways:

1.Purealertingfunctionsinlanechangeassistantsforcars,thetra calertandcollisionavoidancesystem(TCAS)foraircraft;

2.Fine-grainedadaptationsofhumancontrolactionslikestutteringandselectiveforcedistributioninanti-lockbrakingsystemsandelectronicstabilitycontrolforcars;and

3.Semi-automaticcontrolbyspeedsupervisioncontrollersonrailsandcarparkingassis-tants.

Fullyautomaticproactivecontrolhasbecomefeasible.RecentexamplesofthiskindincludetheautomatictrainprotectionunitoftheEuropeantraincontrolsystem(ETCS)andautopilotcontrolforvariousaircraftmaneuveringmodes.Similaradvanceshavebeenachievedinradar-basedadaptivecruisecontrolforcarsthatbrakeautonomouslywhenapproachingtheendofatra cjam.Recentroboticapplicationsevenallowcompletelydriverlessvehiclecontrol.Moregenerally,itturnsoutthatnearlyallmoderntransportationtechnologyde-pendsonatightcouplingwithcomputercontrol.Thismakesthemcyber-physicalsystems(CPS)andhybridsystemswithinteractingdiscreteandcontinuousdynamics.

Soon,therewillbeacompletecoverageofassistancetechnologiesforimportantdriverandpilotdecisions.Simultaneously,theneedforanalysistechniqueshasbecomemorepressing.Either,veri cationtechniqueshavetoensurecorrectfunctioningofsuchsafety-criticalcon-troldevicesordetecterrorsintheirdesignbeforetheycausefatalinjuries.Tragicaccidents

混合系统建模与验证

indicatethattherisingcomplexityoftransportationsystemsmakesitimpossibleforhumanstounderstandtheire ectsandsidee ectsunderallcircumstances.Thisincludes awsinthewarningsystemthatledtothefrontaltraincollisioninChatsworth2008,de cienciesinsomeadaptivecruisecontrollersforcarsfrom2005,andunfortunatehuman-controller¨interactionscausingthefatalmid-aircollisioninUberlingenin2002.

SeverallargeresearchprojectshavebeenlaunchedalreadyinEurope,includingAVACS,ARTIST-2,HYCON,Minalogic,andSPEEDS.WeneedmajorinitiativesfortheUStotakealeadinadvancingthestateoftheartinCPSanalysis.

2ImportantResearchChallengesforCPSTransportation

Theincreasingneedforanalysistechniquesthatscaletotoday’stightlyintegratedtrans-portationcontrolimposesseveralresearchchallengesforCPSanalysisandveri cation.ScalableAnalysiswithrespecttoComplexityandDimensionality:Themostpress-ingneedtodayareanalysistechniquesthatactuallyscaletothefullcomplexityofrealap-plications.Thetwomostfundamentallimitationstodayarethatmostanalysistechniquescanonlyhandlefairlylimitedclassesofsystemdynamics(usuallyonlylinearorevencon-stantdynamics)andthatthedimensionofthecontinuousstatespacetheycanhandleislow(around3-8).Mostapplicationsaregovernedbymorecomplicateddi erentialequations(e.g., ightdynamics)andhavesubstantiallyhigherdimensions(modelsoftheenvironment).Beyondanydoubt,themajorchallengeforhandlingrealistictra csystemsistodeveloptechniquesthatscalereliablybothinthedimensionandcomplexityofthesystemdynamics.Eventoday’shighprecisionanalyseswouldalreadyneednon-lineardynamicsforhundredsofvariables.Iffutureresearchadvancesarenotabletosolvethescalabilityproblem,thegrowingcomplexityofCPScannotbemanagedanymore.Withoutsigni canttechnologicaladvances,weareconvincedthatathoroughsafetyanalysiswillneverbecomepossible!Large-scaleVeri cationArchitecturesforCyber-PhysicalSystems:Tospeeduptheveri cationprocesswithgoodscalabilitypropertiesforindustrialsettings,weenvisionthedevelopmentoflayeredarchitectures.Ratherthanverifyingeachnewtransportationsystemfromscratch,weconsideritmoreeconomicandprobablyevenmoretractabletodevisedomain-speci cveri cationframeworks.Inmuchthesamewayas,e.g.,carsaredesignedasinstancesofaproductfamily,theirsafetyandfailure-robustnessanalysisshouldbeconductedasaspecialinstanceofthegeneralveri cationframeworkforgroundtransportation.Forsuchaframework,acommonparametricsetupcanthenbepre-veri edonceandforall.Eachdesignofaspeci ctra cagentwouldthenonlyneedtobere-analyzedwithrespecttoacorrectinstantiationofthemoregeneralveri cationpattern.Ultimately,weconceivetheformingofVeri cationEngineeringasanewdisciplinedevotedtothesystematicdevelopmentanduseofcorrespondingdomain-speci cveri cationplans.

DynamicNetworksofCyber-PhysicalSystems:Adi erentresearchchallengeresultsfromtheoverwhelmingincreaseofwirelesscommunicationintransportationandtheresult-ingconsequencesfortheoverallsystemscope.AlreadyincurrentimplementationsofETCS,GSM-basedwirelessistheexclusivecommunicationchannelforestablishingconsentastowhichtrainisallowedtomovehowfaronwhichtrack.Similarly,theupcomingCAR2CAR

混合系统建模与验证

standardforco-operativecarcommunicationstrivestousewirelessadhocnetworkstopre-ventroadaccidentsandcircumventtra cjams.Consequently,wenolonger nda xedstaticsetupoftra cagents.Instead,tra cagentsformafullydynamicnetworkofphysi-callymovinghybridsystemswithdynamicallychanginglogicalcommunicationtopology.TheprimaryresearchchallengecausedbyCPSwithdynamictopologyisthatthenumberofparticipantscanchangeovertime,sothatnoteventhedimensionofthesystemstatespaceremainsconstantduringitsevolution.Newveri cationtechniquesareinorderthatcanhandlearbitrarydimensionalityadjustmentsduringsystemtransitions.Withouttheseadvances,analysistechniqueswillneverbeapplicabletonextgenerationtransportationsystems,sothatthehighpotentialofmoderncommunicationtechnologycouldneverbeusedforsafety-criticaltransportation.

ProbabilisticE ectsinCyber-PhysicalTransportation:Afurtherchallengeisau-tomaticstochasticanalysisofthelikelihoodofacertaineventhappeningwhentakingtheprobabilitydistributionofthecorrespondingtransitionsintheCPSintoaccount.Forin-stance,atraininETCSmaystopmovingcompletelywhenallwirelesscommunicationchannelssu erfrom100%packetlosssothatthetraincannotreceivemovementnegotiationmessages.Thisisextremelyunlikely,though.Thequestionis:Isthereanautomaticalgo-rithmfordeterminingtheprobabilityofatrainreachingitsdestinationintime,given,e.g.,acertainmessagelossprobabilityandaparticularrepetitivesendingscheme.Moregenerally,isthereanautomatictoolthatcanprovethatthefailureprobabilityinastochasticCPSisbounded?Likewise,canweanalyzestochasticenvironmentmodelsandsensorfailureprob-abilities?TheprimaryresearchchallengeforstochasticCPSveri cationisto ndanalysistechniquesthatcanhandletheircouplingofstochasticandhybriddynamicsystembehav-iorbyanalyzingthetransformationofappropriateprobabilitydistributionsduringhybridevolutions.ThistechnologywillbeoftremendousimportanceforconductingaformalriskanalysisinfutureCPSfortransportation.

3BiographicalInformation

EdmundM.ClarkeisaUniversityProfessoratCarnegieMellonUniversityandFORESys-temsProfessorintheSchoolofComputerScience.Amongseveralotherawards,hereceivedtheACMKanellakisAward,theIEEEHarryH.GoodeMemorialAward,theACMTuringAward,andtheCADEHerbrandAward.

BruceKroghisaProfessorintheDepartmentofElectricalandComputerEngineeringatCarnegieMellonUniversity.HewasthefoundingEditor-in-ChiefoftheIEEETransactionsonControlSystemsTechnology.Dr.KroghisaDistinguishedMemberoftheIEEEControlSystemsSocietyandaFellowoftheIEEE.

Andr´ePlatzerisanAssistantProfessorintheComputerScienceDepartmentatCarnegieMellonUniversity,Pittsburgh,PA.Amongotherawards,hereceivedthebestpaperawardatTABLEAUX2007andtheWoodyBledsoeAwardatIJCAR2006.

RajRajkumarisaProfessorintheDepartmentofElectricalandComputerEngineeringatCarnegieMellonUniversity.HeisDirectoroftheReal-TimeandMultimediaSystemsLabandCo-DirectoroftheGeneralMotors-CarnegieMellonCollaborativeResearchLabsonInformationTechnologyandonAutonomousDriving.

本文来源：https://www.bwwdw.com/article/o9c4.html