Automated Verification and Refinement for Physical-Layer Protocols

• ABSTRACT:
  
  This paper demonstrates how to use a satisfiability modulo theories (SMT) solver together with a bounded model checker to verify properties of real-time physical layer protocols. The method is first used to verify the Biphase Mark protocol, a protocol that has been verified numerous times previously, allowing for a comparison of results. The techniques are extended to the 8N1 protocol used in universal asynchronous receiver transmitters (UARTs). We then demonstrate the use of temporal refinement to link a finite state specification of 8N1 with its real-time implementation. This refinement relationship relieves a significant disadvantage of SMT approaches---their inability to scale to large problems.

• BIBTEX:
  

  @Article{brownpikefac,
    author =       {Geoffrey Brown and Lee Pike},
    title =        {Automated Verification and Refinement for Physical-Layer Protocols},
    journal =      {Formal Aspects of Computing},
    OPTyear =      {},
    OPTvolume =    {},
    OPTnumber =    {},
    OPTpages =     {},
    OPTmonth =     {},
    note =         {Accepted for publication.  Available at \url{http://www.cs.indiana.edu/~lepike/pub_pages/bmp-jrnl.html}},
  }
  

• PAPER DOWNLOAD: saljrnl.pdf

• SAL FILES DOWNLOAD:
  
  
  • 8N1 protocol SAL model and verification: uartJrnl.sal
  • Biphase Mark protocol SAL model and verification: biphaseJrnl.sal
  • runproof (proof script)

  ---

  Lee Pike (home)