Analysis and Verification Challenges Cyber-Physical Transpor(3)

混合系统建模与验证

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.