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.