Loading...
Please wait, while we are loading the content...
Similar Documents
A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Moore, J. Strother |
| Copyright Year | 1992 |
| Description | In this paper we present a formal model of asynchronous communication as a function in the Boyer-Moore logic. The function transforms the signal stream generated by one processor into the signal stream consumed by an independently clocked processor. This transformation 'blurs' edges and 'dilates' time due to differences in the phases and rates of the two clocks and the communications delay. The model can be used quantitatively to derive concrete performance bounds on asynchronous communications at ISO protocol level 1 (physical level). We develop part of the reusable formal theory that permits the convenient application of the model. We use the theory to show that a biphase mark protocol can be used to send messages of arbitrary length between two asynchronous processors. We study two versions of the protocol, a conventional one which uses cells of size 32 cycles and an unconventional one which uses cells of size 18. We conjecture that the protocol can be proved to work under our model for smaller cell sizes and more divergent clock rates but the proofs would be harder. |
| File Size | 2587862 |
| Page Count | 60 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_19920018343 |
| Archival Resource Key | ark:/13960/t5n925g1r |
| Language | English |
| Publisher Date | 1992-06-01 |
| Access Restriction | Open |
| Subject Keyword | Cycles Fault Tolerance Protocol Computers Messages Theorem Proving Synchronism Logic Design Program Verification Computers Transformations Mathematics Clocks 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 |
