MARC

 008260203s2023        us                              c    eng  d
■001000017365853
■00520260209102839
■006m          o    d                
■007cr#unu||||||||
■020    ▼a9798314843581
■035    ▼a(MiAaPQ)AAI32063785
■035    ▼a(MiAaPQ)httphdlhandlenet2142120127
■040    ▼aMiAaPQ▼cMiAaPQ
■0820  ▼a004
■1001  ▼aHsieh,  Chiao.
■24510▼aAbstractions  for  Safety  Assurance  of  Autonomous  Systems
■260    ▼a[Sl]▼bUniversity  of  Illinois  at  Urbana-Champaign▼c2023
■260  1▼aAnn  Arbor▼bProQuest  Dissertations  &  Theses▼c2023
■300    ▼a163  p
■500    ▼aSource:  Dissertations  Abstracts  International,  Volume:  86-11,  Section:  B.
■500    ▼aAdvisor:  Mitra,  Sayan.
■5021  ▼aThesis  (Ph.D.)--University  of  Illinois  at  Urbana-Champaign,  2023.
■520    ▼aAn  autonomous  system  has  components  to  perceive  the  environment,  control  the  hardware,  and  communicate  with  other  agents.  Ideally,  the  formal  analysis  of  the  closed-loop  system  would  have  access  to  explicit  models  of  all  components.  However,  explicit  models  of  perception  and  dynamics  are  often  unavailable  or  intractable  for  formal  verification.  Instead,  executable  models  for  these  components  are  available  for  simulation  and  testing  in  practice.  In  this  thesis,  we  will  present  our  compositional  verification  framework  for  certifying  and  assuring  safety  for  systems  with  combinations  of  distributed  communication,  learning-enabled  perception,  and  black-box  dynamics.  Our  insight  is  to  construct  abstractions  of  these  components  for  the  end-to-end  system-level  safety  analysis;  then  we  empirically  validate  each  component  against  its  abstraction  by  sampling  executable  models.For  distributed  robotic  applications,  we  focus  on  constructing  the  abstraction  for  heterogeneous  motion  dynamics.  Our  notion  of  port  assumptions  for  dynamics  decomposes  the  safety  assurance  into  two  steps:  (a)  the  formal  safety  proof  of  the  distributed  system  using  port  assumptions,  and  (b)  the  validation  of  port  assumptions  using  data-driven  reachability  analyses.  We  learned  that  this  compositional  reasoning  generalizes  to  both  synchronous  and  asynchronous  communications  between  heterogeneous  vehicles.  We  are  able  to  derive  the  collision  avoidance  guarantee  in  a  distributed  delivery  application  using  our  Koord  framework  for  shared  variable  communication  between  ground  vehicles  and  quadrotors.  We  apply  the  same  idea  on  asynchronous  message  passing-based  Unmanned  Air-traffic  Management  protocols  (UTM)  and  verify  safe  separations  between  quadrotors  and  fixed-wing  airplanes.We  also  study  autonomous  systems  with  visual  perception  enabled  by  deep  neural  networks  (DNNs).  Our  main  insight  is  to  search  for  ground  truth-based  approximate  abstractions  for  perception.  Our  notion  of  approximate  abstractions  bypasses  the  challenges  in  the  formal  specification  of  perception  and  high  dimensional  image  domains,  and  the  precision  of  the  approximate  abstraction  can  be  estimated  empirically.  We  study  both  single  agent  and  multiagent  systems  including  three  practical  vision-based  autonomous  systems:  (a)  a  lane  tracking  system  for  an  autonomous  vehicle,  (b)  a  corn  row  following  system  for  an  agricultural  robot,  and  (c)  a  vision-based  multi-agent  swarm  formation.  We  are  able  to  provide  end-to-end  assurance  for  all  systems  and  examine  the  precision  using  simulations.In  summary,  our  compositional  verification  framework  outlines  a  pragmatic  path  to  provide  safety  assurance  of  autonomous  systems.  We  formalize  (approximate)  abstractions  for  compositional  verification  and  develop  approaches  to  search  for  abstractions.  This  allows  us  to  formally  verify  as  many  components  in  the  system  as  possible.  For  other  components  that  are  intractable  for  formal  verification,  we  search  for  abstractions  of  these  components  and  rigorously  validate  the  abstractions  via  testing  and  data-driven  verification.  We  are  able  to  gain  safety  assurance  using  abstractions  in  all  our  case  studies  and  validate  the  abstractions  with  high-fidelity  Gazebo  and  AirSim  simulations.
■590    ▼aSchool  code:  0090.
■650  4▼aComputer  science
■650  4▼aEngineering
■650  4▼aInformation  technology
■653    ▼aAutonomous  systems
■653    ▼aSafety  assurance
■653    ▼aFormal  verification
■653    ▼aCompositional  verification
■653    ▼aDistributed  robotics
■653    ▼aLearning-enabled  systems
■690    ▼a0984
■690    ▼a0489
■690    ▼a0800
■690    ▼a0537
■71020▼aUniversity  of  Illinois  at  Urbana-Champaign▼bComputer  Science.
■7730  ▼tDissertations  Abstracts  International▼g86-11B.
■790    ▼a0090
■791    ▼aPh.D.
■792    ▼a2023
■793    ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T17365853▼nKERIS▼z이  자료의  원문은  한국교육학술정보원에서  제공합니다.

Preview

Export

ChatGPT Discussion

AI Recommended Related Books