NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login
Back to Results
A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocolIn 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.
Document ID
19920018343
Acquisition Source
Legacy CDMS
Document Type
Contractor Report (CR)
Authors
Moore, J. Strother (Computational Mechanics Co. Austin, TX, United States)
Date Acquired
September 6, 2013
Publication Date
June 1, 1992
Publication Information
Publisher: NASA. Langley Research Center
Subject Category
Computer Systems
Report/Patent Number
NASA-CR-4433
TR-68
NAS 1.26:4433
Accession Number
92N27586
Funding Number(s)
PROJECT: RTOP 505-64-10-05
CONTRACT_GRANT: NAS1-18878
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.

Related Records

There are no records associated with this record.
No Preview Available