[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php

Bibliographic Item (1.0)

KayReed93

  1. Andrew Kay & Joy N Reed
  2. A Rely and Guarantee Method for Timed CSP: A Specification and Design of a Telephone Exchange
  3. IEEE Trans SE-V19n6(Jun 1993)pp625-639
  4. =THEORY MODULES NONSEQUENTIAL SAFETY LIVENESS PROOF PERFORMANCE
      p631: "The correctness proofs for the design require that the time for internal signal be very small compared to times between externally generated signals." need expertise to recognise and handle race conditions

      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.

    1. TCSP::=Timed CSP traces with refusal sets - research/1 notes/kay&reed/... prevents, causes,

      rely and guarantee

      P O T S: Spec with 24 rely/guarantee pairs



Search for bibliographic items containing a matching string.


(Search uses POSIX regular expressions and ignores case)

Search for a specific bibliographic item by name.



To see the complete bibliography (1Mb+) select:[Bibliography]