MARC

 008250123s2024        us                              c    eng  d
■001000017161445
■00520250211151357
■006m          o    d                
■007cr#unu||||||||
■020    ▼a9798382841991
■035    ▼a(MiAaPQ)AAI31243926
■040    ▼aMiAaPQ▼cMiAaPQ
■0820  ▼a004
■1001  ▼aNi,  Haobin.▼0(orcid)0000-0002-7718-7905
■24510▼aFormal  Modeling  Languages  for  High-assurance  Domain-specific  Systems  ▼b高保障特定领域系统的形式化建模语言
■260    ▼a[Sl]▼bCornell  University▼c2024
■260  1▼aAnn  Arbor▼bProQuest  Dissertations  &  Theses▼c2024
■300    ▼a201  p
■500    ▼aSource:  Dissertations  Abstracts  International,  Volume:  85-12,  Section:  B.
■500    ▼aAdvisor:  Morrisett,  John.
■5021  ▼aThesis  (Ph.D.)--Cornell  University,  2024.
■520    ▼aSoftware  systems  today  struggle  to  behave  as  intended  in  deployment.  The  problem  is  made  worse  by  the  ever-increasing  complexity  of  systems  resulting  from  the  rapid  expansion  of  modern-day  software.  For  instance,  almost  all  systems  nowadays  utilize  concurrency,  and  unexpected  behaviors  such  as  race  conditions  are  quite  common.  In  this  case  and  many  others,  the  number  of  possible  program  behaviors  suffers  from  combinatorial  explosion,  which  renders  conventional  testing  insufficient  to  provide  enough  assurance  at  a  feasible  cost.This  dissertation  explores  alternative  approaches  that  guarantee  high  assurance  systematically  and  foundationally  by  building  and  analyzing  formal  models  of  those  systems  through  domain-specific  languages.  While  real-world  systems  often  involve  components  of  many  different  domains,  as  a  first  step,  we  choose  three  mission-critical  domains  as  targets:  fault-tolerant  distributed  protocols,  concurrent  programs,  and  parsers.  For  each  of  those  domains,  a  new  language  for  formally  modeling  domain-specific  systems  is  proposed.  Meta-theoretic  analyses  of  those  languages  illustrate  the  relationships  between  models  built  in  those  languages  and  the  realistic  behaviors  of  the  systems  those  models  describe,  guaranteeing  that  all  those  formal  models  are  adequate  for  analyzing  system  behaviors.  Case  studies  of  systems  modeled  and  analyzed  using  those  languages  are  also  presented  to  demonstrate  the  effectiveness  of  this  approach  and  the  developed  tools  in  constructing  high-assurance  domain-specific  systems.
■590    ▼aSchool  code:  0058.
■650  4▼aComputer  science
■650  4▼aComputer  engineering
■650  4▼aSystems  science
■653    ▼aConcurrent  systems
■653    ▼aDistributed  systems
■653    ▼aFormal  method
■653    ▼aProgramming  language
■653    ▼aSyntactic  analysis
■653    ▼aVerification
■690    ▼a0984
■690    ▼a0464
■690    ▼a0790
■71020▼aCornell  University▼bComputer  Science.
■7730  ▼tDissertations  Abstracts  International▼g85-12B.
■790    ▼a0058
■791    ▼aPh.D.
■792    ▼a2024
■793    ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T17161445▼nKERIS▼z이  자료의  원문은  한국교육학술정보원에서  제공합니다.

Preview

Export

ChatGPT Discussion

AI Recommended Related Books