混合系统建模与验证

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