Paper Details

@InProceedings{McEwan06,
  title = "{A} {C}ircus {D}evelopment and {V}erification of an {I}nternet {P}acket {F}ilter.",
  author= "McEwan, Alistair A.",
  editor= "Welch, Peter H. and Kerridge, Jon and Barnes, Frederick R. M.",
  pages = "339--362",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2006",
  isbn= "978-1-58603-671-3",
  year= "2006",
  month= "sep",
  abstract= "In this paper, we present the results of a significant and
     large case study in Circus. Development is top-down - from a
     sequential abstract specification about which safety
     properties can be verified, to a highly concurrent
     implementation on a Field Programmable Gate Array.
     Development steps involve applying laws of Circus allowing
     for the refinement of specifications; confidence in the
     correctness of the development is achieved through the
     applicability of the laws applied; proof obligations are
     discharged using the model-checker for CSP, FDR, and the
     theorem prover for Z, Z/Eves. An interesting feature of this
     case study is that the design of the implementation is
     guided by domain knowledge of the application - the
     application of this domain knowledge is supported by, rather
     than constrained by the calculus. The design is not what
     would have been expected had the calculus been applied
     without this domain knowledge. Verification highlights a
     curious error made in early versions of the implementation
     that were not detected by testing."
}

If you have any comments on this database, including inaccuracies, requests to remove or add information, or suggestions for improvement, the WoTUG web team are happy to hear of them. We will do our best to resolve problems to everyone's satisfaction.

Copyright for the papers presented in this database normally resides with the authors; please contact them directly for more information. Addresses are normally presented in the full paper.