Easy Parameterized Verificaton of Biphase Mark and 8N1 Protocols

• ABSTRACT:
  
  The Biphase Mark Protocol (BMP) and 8N1 Protocol are physical layer protocols for data transmission. We present a generic model in which timing and error values are parameterized by linear constraints, and then we use this model to verify these protocols. The verifications are carried out using SRI's SAL model checker that combines a satisfiability modulo theories decision procedure with a bounded model checker for highly-automated induction proofs of safety properties over infinite-state systems. Previously, parameterized formal verification of real-time systems required mechanical theorem-proving or specialized real-time model checkers; we describe a compelling case-study demonstrating a simpler and more general approach. The verification reveals a significant error in the parameter ranges for 8N1 given in a published application note.

• BIBTEX:
  

  @InProceedings{brown_pike_06,
    author =    {Geoffrey M. Brown and Lee Pike},
    title =     {Easy parameterized verification of biphase mark and {8N1} protocols},
    booktitle = {The Proceedings of the 12th International Conference on Tools and the 
                 Construction of Algorithms ({TACAS'06})},
    year =      {2006},
    publisher = {Springer},
    series    = {Lecture Notes in Computer Science},
    volume    = {3920},
    pages =     {58--72},
    note =      {Available at \url{https://leepike.github.io/pub_pages/bmp.html}}}
  

• PAPER DOWNLOAD: pdf 

• SLIDES DOWNLOAD: pdf

• SAL FILES DOWNLOAD:
  
  
  • uart.sal
  • biphase.sal
  • biphase_full.sal (fully parameterized model)
  • runproof (proof script)

• ADDENDUM:
  
  The paper mentions a shortcoming with the ICS decision procedure that prevents a substantially parameterized 8N1 protocol from being verified. We discovered a solution to this shortcoming that involves restating the main disjunctive invariant in terms of a recursive function, and using a recursive function as a "macro" for multiplication. Under this reformulation, a parameterized verification with error terms and a fully parameterized verification are successfully verified.
  
  
• uart_rec.sal (model with error terms)
• uart_full.sal (fully parameterized model)

• NOTES: The SMT verification conditions from this work are some of the SMT-LIB quantifier-free linear real-arithmetic benchmarks.