Reasoning About Conditional Progress Properties

Show simple item record

dc.contributor.author Calvert, Kenneth L. en_US
dc.date.accessioned 2005-06-17T17:57:28Z
dc.date.available 2005-06-17T17:57:28Z
dc.date.issued 1994 en_US
dc.identifier.uri http://hdl.handle.net/1853/6709
dc.description.abstract In 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.extent 246644 bytes
dc.format.mimetype application/pdf
dc.language.iso en_US
dc.publisher Georgia Institute of Technology en_US
dc.relation.ispartofseries CC Technical Report; GIT-CC-94-03 en_US
dc.subject Communication protocols
dc.subject Distributed systems
dc.subject Data transmission
dc.title Reasoning About Conditional Progress Properties en_US
dc.type Technical Report eng_US


Files in this item

Files Size Format View
GIT-CC-94-03.pdf 240.8Kb PDF View/ Open

This item appears in the following Collection(s)

Show simple item record