Automated verification and refinement for physical-layer protocols

作者：Brown Geoffrey M^*; Pike Lee

来源：Formal Aspects of Computing, 2011, 23(3): 243-266.

DOI：10.1007/s00165-010-0149-0

• Satisfiability modulo theories (SMT)
• Infinite-state model checking
• Real-time
• Physical layer
• Biphase Mark
• UART

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. 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. Finally, capturing the impact of metastability on timing requirements is a key issue in modeling physical-layer protocols. Rather than model metastability directly, a contribution of our models is treating its effect as a constraint on non-determinism.

• 出版日期2011-5