A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
- Moore, J. Strother
- Jun 1, 1992.
- Physical Description:
- 1 electronic document
- Restrictions on Access:
- Unclassified, Unlimited, Publicly available.
- 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.
- NASA Technical Reports Server (NTRS) Collection.
- Document ID: 19920018343., Accession ID: 92N27586., NASA-CR-4433., TR-68., and NAS 1.26:4433.
- No Copyright.
View MARC record | catkey: 15675227