Formally Verifying Hybrid Protocols with the Nuprl Logical ProgrammingEnvironment
Loading...
No Access Until
Permanent Link(s)
Collections
Other Titles
Abstract
We describe a generic switching protocol for the construction of hybrid protocols and prove it correct with the Nuprl proof development system. We introduce the concept of meta-properties to characterize communication properties that can be preserved by switching and identify switching invariants that an implementation of the switching protocol must satisfy in order to work correctly. Our work shows how a theorem prover with a rich specification language can contribute to the design and implementation of verifiably correct adaptive protocols and that it can have a large impact when being engaged at the earliest stages of the design.
Journal / Series
Volume & Issue
Description
Sponsorship
Date Issued
2001-05-09
Publisher
Cornell University
Keywords
computer science; technical report
Location
Effective Date
Expiration Date
Sector
Employer
Union
Union Local
NAICS
Number of Workers
Committee Chair
Committee Co-Chair
Committee Member
Degree Discipline
Degree Name
Degree Level
Related Version
Related DOI
Related To
Related Part
Based on Related Item
Has Other Format(s)
Part of Related Item
Related To
Related Publication(s)
Link(s) to Related Publication(s)
References
Link(s) to Reference(s)
Previously Published As
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR2001-1839
Government Document
ISBN
ISMN
ISSN
Other Identifiers
Rights
Rights URI
Types
technical report