MARC

 008260126s2025        us                              c    eng  d
■001000017357221
■00520260202103150
■006m          o    d                
■007cr#unu||||||||
■020    ▼a9798288863103
■035    ▼a(MiAaPQ)AAI31996613
■040    ▼aMiAaPQ▼cMiAaPQ
■0820  ▼a621.3
■1001  ▼aYu,  Sheng-Jung.
■24510▼aAutomating  Contract-Based  Design  for  Cyber-Physical  Systems
■260    ▼a[Sl]▼bUniversity  of  California,  Berkeley▼c2025
■260  1▼aAnn  Arbor▼bProQuest  Dissertations  &  Theses▼c2025
■300    ▼a210  p
■500    ▼aSource:  Dissertations  Abstracts  International,  Volume:  87-01,  Section:  B.
■500    ▼aAdvisor:  Sangiovanni-Vincentelli,  Alberto.
■5021  ▼aThesis  (Ph.D.)--University  of  California,  Berkeley,  2025.
■520    ▼aCyber-physical  systems  (CPS),  which  integrate  computational  and  physical  processes,  present  challenges  in  modeling,  specification,  and  integration  due  to  their  heterogeneous  nature  and  complex  interactions.  Contract-based  design  aims  to  address  these  challenges  by  using  formal  specifications  to  support  hierarchical  decomposition  and  system-level  reasoning  through  contract  manipulations.  Combining  this  methodology  with  design  automation,  which  leverages  computational  power  to  streamline  design  tasks,  offers  a  promising  approach  to  addressing  the  CPS  design  challenges.This  dissertation  focuses  on  automating  the  contract-based  design  process  to  facilitate  its  application  in  cyber-physical  system  design.  We  identify  the  key  design  automation  needs  for  contract-based  design  as  specification,  verification,  simulation,  and  synthesis.  Specification  enables  the  expression  of  requirements  and  implementations  as  contracts  while  assisting  in  their  manipulation.  Verification  detects  potential  errors  in  the  decomposition  process,  ensuring  a  correct-by-construction  design.  Simulation  provides  insight  into  formal  specifications  by  generating  behaviors  allowed  by  their  semantics,  helping  designers  confirm  that  contracts  align  with  design  intent  and  component  characteristics.  Synthesis  automates  the  decomposition  process  and  optimizes  the  design.We  address  these  needs  by  bridging  key  gaps  in  contract-based  design  automation.  For  specification,  a  new  contract  formalism,  constraint-behavior  contracts,  is  introduced  to  represent  physical  components  using  implicit  equations,  enabling  precise  expression  of  requirements.  Verification  techniques  based  on  receptiveness  and  strong  replaceability,  a  newly  proposed  contract  relation,  are  developed  to  detect  decomposition  errors,  including  in  feedback  systems,  ensuring  correct-by-construction  designs.  We  also  propose  a  simulation  framework  that  generates  behaviors  allowed  by  contract  semantics  and  efficiently  produces  a  small  yet  insightful  set  of  examples  to  aid  in  validating  contracts  and  localizing  potential  specification  errors.  A  component  selection  algorithm  combining  black-box  optimization  with  contract-based  system  reasoning  is  proposed  to  incorporate  behaviors  into  the  decomposition  process  and  enable  contract-based  synthesis  that  addresses  optimization  objectives  involving  behaviors.We  integrate  these  contributions  into  ContractDA,  the  first  tool  for  contract-based  design  to  offer  comprehensive  design  automation  support,  including  specification,  verification,  simulation,  and  synthesis.  ContractDA  incorporates  the  proposed  functionalities  along  with  existing  contract  manipulations,  offering  an  interface  that  enables  designers  and  researchers  to  effectively  apply  contract-based  design.
■590    ▼aSchool  code:  0028.
■650  4▼aElectrical  engineering
■650  4▼aComputer  science
■650  4▼aInformation  technology
■653    ▼aContract-based  design
■653    ▼aCyber-physical  system
■653    ▼aDesign  automation
■653    ▼aFormal  method
■690    ▼a0544
■690    ▼a0984
■690    ▼a0489
■71020▼aUniversity  of  California,  Berkeley▼bElectrical  Engineering  &  Computer  Sciences.
■7730  ▼tDissertations  Abstracts  International▼g87-01B.
■790    ▼a0028
■791    ▼aPh.D.
■792    ▼a2025
■793    ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T17357221▼nKERIS▼z이  자료의  원문은  한국교육학술정보원에서  제공합니다.

Preview

Export

ChatGPT Discussion

AI Recommended Related Books