Loading...
Please wait, while we are loading the content...
Similar Documents
Design and verification of a distributed communication protocol
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Goodloe, Alwyn E. Munoz, Cesar A. |
| Copyright Year | 2009 |
| Description | The safety of remotely operated vehicles depends on the correctness of the distributed protocol that facilitates the communication between the vehicle and the operator. A failure in this communication can result in catastrophic loss of the vehicle. To complicate matters, the communication system may be required to satisfy several, possibly conflicting, requirements. The design of protocols is typically an informal process based on successive iterations of a prototype implementation. Yet distributed protocols are notoriously difficult to get correct using such informal techniques. We present a formal specification of the design of a distributed protocol intended for use in a remotely operated vehicle, which is built from the composition of several simpler protocols. We demonstrate proof strategies that allow us to prove properties of each component protocol individually while ensuring that the property is preserved in the composition forming the entire system. Given that designs are likely to evolve as additional requirements emerge, we show how we have automated most of the repetitive proof steps to enable verification of rapidly changing designs. |
| File Size | 264670 |
| Page Count | 33 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_20090014785 |
| Archival Resource Key | ark:/13960/t50g8nc76 |
| Language | English |
| Publisher Date | 2009-01-04 |
| Access Restriction | Open |
| Subject Keyword | Iteration Protocol Computers Losses Safety Proving Ntrs Nasa Technical Reports Server (ntrs) Nasa Technical Reports Server Aerodynamics Aircraft Aerospace Engineering Aerospace Aeronautic Space Science |
| Content Type | Text |
| Resource Type | Technical Report |
