Temporal Refinement Using SMT and Model Checking with an Application to Physical-Layer Protocols

• ABSTRACT:
  
  This paper demonstrates how to use a satisfiability modulo theories (SMT) solver together with a bounded model checker to complete highly-automated temporal refinement proofs. The method is demonstrated by refining a specification of the 8N1 Protocol, a widely-used protocol for serial data transmission. A nondeterministic finite-state 8N1 specification is refined to an infinite-state implementation in which interleavings are constrained by real-time linear inequalities. The refinement proof is via automated induction proofs over infinite-state transitions systems using SMT and model checking, as implemented in SRI International's Symbolic Analysis Laboratory (SAL).

• BIBTEX:
  

  @inproceedings{brown_pike:memocode,
    author = {Geoffrey Brown and Lee Pike},
    title = {Temporal Refinement Using SMT and Model Checking with an Application to Physical-Layer Protocols},
    booktitle = {Proceedings of Formal Methods and Models for Codesign (MEMOCODE'2007)},
    year = {2007},
    pages = {171--180},
    location = {Nice, France},
    publisher = {OmniPress},
    note = {Available at \url{https://leepike.github.io/pub_pages/refinement.html}}}
  

• PAPER DOWNLOAD: pdf 

• SLIDES DOWNLOAD: pdf

• SAL FILES DOWNLOAD:
  
  
  • Finite-state and infinite-state 8N1 Protocol models:
  • uart.sal (infinite-state model with correctness proof using SAL's BDD model checker)
  • untimeduart.sal (finite-state model with refinement proofs using SAL's infinite-bmc induction prover)
  • Finite-state and infinite-state Biphase Mark Protocol models:
  • biphase.sal (infinite-state model with correctness proof using SAL's BDD model checker)
  • untimedbiphase.sal (finite-state model with refinement proofs using SAL's infinite-bmc induction prover)
  • Finite-state and infinite-state 8N1 Protocol models with shift-registers:
  • uart_reg.sal (infinite-state model with correctness proof using SAL's BDD model checker)
  • untimeduart_reg.sal (finite-state model with refinement proofs using SAL's infinite-bmc induction prover)
  • runproof (proof script)