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 M. Brown and Lee Pike},
    title     = {Automated verification and refinement for physical-layer protocols},
    journal   = {Formal Aspects of Computing},
    volume    = {23},
    number    = {3},
    year      = {2011},
    pages     = {243-266},
    note = {Available at \url{https://leepike.github.io/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)