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{http://www.cs.indiana.edu/~lepike/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)

Lee Pike (home) |