|
|
 |
|
NIA Formal Methods Seminar by Lee Pike |
|
Date: November 2, 2006
Time: 10:30am
Location: NASA Langley Research Center, Building 1220, Room 110
Temporal Refinement Using SMT and Model Checking with an Application to Physical-Layer Protocols
Lee Pike, Galois Connections
This talk 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).
|
|
|
Home