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

Bibliographic Item (1.0)

CreveuilRoman94

  1. Christian Creveuil & Gruia-Catalin Roman
  2. Formal Specification and Design of a Message Router
  3. ACM Trans Softw Eng Methodol V3n4(Oct 1994)pp271-307 CR9512-0963
  4. =CASE-STUDY UNITY FORMAL NONSEQUENTIAL CASESTUDY
  5. Router problem studied in the 6th International Workshop on Software Specification and Design p304-305, Conclusions
    1. "It is better to specify and reason about a closed system - i.e. a system and its environment -- rather than an open one" ...

      "[A] critical element is the formulation of the top-level specification[...] focussing on I/O properties[...]selecting the "right" notation. [..] One does not stumble upon appropriate notation. Experience, exploration, and some looking ahead can provide the required insight. [...] True design, however, never makes such pretense[of being mechanistic]. Looking ahead and back-tracking are a part of the method. [...] selection of auxilary variables was one of the key decisions."

      "[...]small refinements proved helpful."

      "It was relatively easy to separate the formal treatment of the proofs from the refinement process itself. [... many trial refinements,...final design proved]. [...] design and verification can actually be carried out by different people."



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]