[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php
p629: Rely/garantee works without extra conditions as long as: (1)No safety constraints on inputs and (2) every component polls its all its inputs
p638: "Our main objective was to prove that desirable things happen within a given time"
p635: "...proofs often revealed faults in our proposed design" Uses DFD-like diagrams
p630:"The first version of the specification, as is inevitable in any non-trivial application, did undergo a certain amount of change during the design phase"
p625: "Masses of useless formal scribblings" avoided by "CSP specification style of giving predicates over sets of traces of the system (and its components) can result in more abstract specifications than those in a state/transition style, and hence are less detailed" "Components do not have behave correctly in every invironment, but if each component satisfies its individual specification the behavior of the composite system is not compromised" ..."The rely and guarantee parts of the specification are collected to form interface specifications, making for a high level of organisation with the minimum of effort".
Has ref to Cliff Jones D. Phil thesis Oxon Jun 1981 Should have ref to [Lamport90b] perhaps.
rely and guarantee
P O T S: Spec with 24 rely/guarantee pairs
Search for a specific bibliographic item by name.
To see the complete bibliography (1Mb+) select:[Bibliography]