MARC

 008250123s2024        us                              c    eng  d
■001000017164695
■00520250211153032
■006m          o    d                
■007cr#unu||||||||
■020    ▼a9798346760207
■035    ▼a(MiAaPQ)AAI31636302
■040    ▼aMiAaPQ▼cMiAaPQ
■0820  ▼a004
■1001  ▼aYao,  Jianan.
■24510▼aAutomated  Verification  of  Safety  and  Liveness  Properties  for  Distributed  Protocols
■260    ▼a[Sl]▼bColumbia  University▼c2024
■260  1▼aAnn  Arbor▼bProQuest  Dissertations  &  Theses▼c2024
■300    ▼a138  p
■500    ▼aSource:  Dissertations  Abstracts  International,  Volume:  86-06,  Section:  B.
■500    ▼aAdvisor:  Gu,  Ronghui.
■5021  ▼aThesis  (Ph.D.)--Columbia  University,  2024.
■520    ▼aThe  world  relies  on  distributed  systems,  but  these  systems  are  increasingly  complex  and  hard  to  design  and  implement  correctly.  This  is  due  to  the  intrinsic  non-determinism  from  asynchronous  node  communications,  various  failure  scenarios,  and  potentially  adversarial  participants.  To  address  this  problem,  developers  are  starting  to  turn  to  formal  verification  techniques  to  prove  the  correctness  of  distributed  systems.  This  involves  formally  verifying  that  desired  safety  and  liveness  properties  hold  for  the  distributed  protocol.  A  safety  property  is  an  invariant  that  should  hold  true  at  any  point  in  a  system's  execution.  It  ensures  the  protocol  does  not  reach  invalid  or  dangerous  states.  A  liveness  property,  on  the  contrary,  describes  that  some  desired  good  event  will  eventually  happen.  There  have  long  been  efforts  to  formally  verify  safety  and  liveness  of  distributed  protocols.  However,  the  proof  burden  is  usually  prohibitively  high  for  broad  real-world  adoption.  Although  there  has  been  a  growing  list  of  methods  that  try  to  automate  the  verification  of  distributed  protocols,  in  particular  their  safety  properties,  none  of  these  tools  scale  to  real-world  complex  protocols  with  theoretical  guarantee.In  this  dissertation,  I  introduce  our  verification  methods  and  tools  for  verifying  distributed  protocols  with  little  to  no  human  effort.  The  thesis  consists  of  two  parts.  In  the  first  part,  I  present  our  two  inductive  invariant  inference  tools,  DistAI  and  DuoAI,  which  automatically  verify  safety  properties  of  distributed  protocols.  In  DistAI,  I  introduce  a  simulation-enumeration-refinement  framework  for  invariant  reasoning,  and  DuoAI  extends  it  to  more  complex  protocols  and  existential  quantifiers.  The  evaluation  shows  that  DuoAI  outperforms  alternative  methods  in  both  the  number  of  protocols  verified  and  the  speed  to  verify  them,  including  solving  Paxos  more  than  two  orders  of  magnitude  faster  than  any  alternative  method.In  the  second  part,  I  introduce  LVR,  our  liveness  verification  tool  for  distributed  protocols.  The  key  theoretical  insight  is  that  liveness  verification  can  be  soundly  reduced  to  the  verification  of  a  list  of  simpler  safety  properties,  which  can  often  be  proved  automatically  utilizing  an  arsenal  of  invariant  inference  tools.  The  reduction  leaves  one  remaining  task-to  synthesize  a  ranking  function  to  prove  termination,  for  which  I  present  a  new  and  effective  pipeline.  LVR  is  successfully  applied  to  eight  distributed  protocols  and  is  the  first  to  demonstrate  that  liveness  properties  of  distributed  protocols  can  be  proved  with  limited  human  input.
■590    ▼aSchool  code:  0054.
■650  4▼aComputer  science
■650  4▼aComputer  engineering
■650  4▼aInformation  technology
■653    ▼aDistributed  protocols
■653    ▼aFormal  verification
■653    ▼aInvariant  inference
■653    ▼aRanking  function
■653    ▼aLiveness  properties
■690    ▼a0984
■690    ▼a0489
■690    ▼a0464
■71020▼aColumbia  University▼bComputer  Science.
■7730  ▼tDissertations  Abstracts  International▼g86-06B.
■790    ▼a0054
■791    ▼aPh.D.
■792    ▼a2024
■793    ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T17164695▼nKERIS▼z이  자료의  원문은  한국교육학술정보원에서  제공합니다.

Preview

Export

ChatGPT Discussion

AI Recommended Related Books