| 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. |
|---|---|
| Creator(s): | |
| Creation Date: | March 1, 1939 |
| Partner(s): |
UNT Libraries Government Documents Department
|
| Collection(s): |
National Advisory Committee for Aeronautics Collection
Technical Report Archive and Image Library
|
| Usage: |
Total Uses: 23
Past 30 days: 3
Yesterday: 0
|
| Creator (Author): |
|
|
|---|---|---|
| Creator (Author): | ||
| Date(s): |
|
|
| 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. |
|
| Language(s): | ||
| Subject(s): |
|
|
| Keyword(s): | aeronautics (general) | |
| Contributor(s): | ||
| Serial Title: | NACA Special Report | |
| Partner: |
UNT Libraries Government Documents Department
|
|
| Collection: |
National Advisory Committee for Aeronautics Collection
|
|
| Collection: |
Technical Report Archive and Image Library
|
|
| Identifier: |
|
|
| Resource Type: | Report | |
| Format: | Text | |
| Rights: |
Access:
Public
License:
Public Domain
Statement:
No Copyright, Unclassified, Unlimited, Publicly available
|
|
