Name
Abstract | ||
|---|---|---|
The Biphase Mark Protocol (BMP) and 8N1 Protocol are physical layer protocols for data transmission. We present a generic model in which timing and error values are parameterized by linear constraints, and then we use this model to verify these protocols. The verifications are carried out using SRI's SAL model checker that combines a satisfiability modulo theories decision procedure with a bounded model checker for highly-automated induction proofs of safety properties over infinite-state systems. Previously, parameterized formal verification of real-time systems required mechanical theorem-proving or specialized real-time model checkers; we describe a compelling case-study demonstrating a simpler and more general approach. The verification reveals a significant error in the parameter ranges for 8N1 given in a published application note [1]. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1007/11691372_4 | TACAS |
Keywords | Field | DocType |
real time,physical layer,formal verification,data transmission,theorem proving,satisfiability modulo theories,real time systems | Parameterized complexity,Model checking,Computer science,Satisfiability,Automated theorem proving,Algorithm,Proof theory,Satisfiability modulo theories,Bounded function,Formal verification | Conference |
Volume | ISSN | ISBN |
3920 | 0302-9743 | 3-540-33056-9 |
Citations | PageRank | References |
22 | 1.36 | 10 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Geoffrey M. Brown | 1 | 225 | 36.38 |
| Lee Pike | 2 | 90 | 6.90 |