Show simple item record

dc.contributor.authorCalvert, Kenneth L.en_US
dc.date.accessioned2005-06-17T17:57:28Z
dc.date.available2005-06-17T17:57:28Z
dc.date.issued1994en_US
dc.identifier.urihttp://hdl.handle.net/1853/6709
dc.description.abstractIn some otherwise attractive formalisms, it can be difficult or even impossible to specify progress in such a way that a component of a distributed system can be proved correct independent of its environment. This problem arises because the nested dependencies between the component and its environment cannot be conveniently expressed in the formalism. A typical example is a communication protocol, which is supposed to provide reliable data transfer even over channels that are unboundedly lossy: the channels only deliver messages if the protocol transmits them often enough, while the protocol only guarantees reliable service if the channels deliver sufficiently many messages. This paper investigates the extent to which such progress specifications can be dealt with using predicate calculus and a single temporal operator (leads-to) having a simple proof theory. It turns out that under the proper semantic interpretation, many progress specifications expressing complex dependences can be represented using certain boolean combinations of leads-to properties. By adding two simple inference rules to an existing proof theory, we obtain a (relatively) complete theory for a large class of conditional progress properties, without the complexity of the full temporal logic; such a theory can be used with various compositional specification formalisms. Based on the results, an approach to specification of protocol progress is outlined and illustrated with an example.en_US
dc.format.extent246644 bytes
dc.format.mimetypeapplication/pdf
dc.language.isoen_US
dc.publisherGeorgia Institute of Technologyen_US
dc.relation.ispartofseriesCC Technical Report; GIT-CC-94-03en_US
dc.subjectCommunication protocols
dc.subjectDistributed systems
dc.subjectData transmission
dc.titleReasoning About Conditional Progress Propertiesen_US
dc.typeTechnical Reporteng_US


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record