Automated Verification and Refinement for Physical-Layer
msra
摘要
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. 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 eect as a constraint on non-determinism.
更多查看译文
关键词
infinite-state model checking,uart,physical layer,real-time,satisfiability modulo theories smt,biphase mark
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络