db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
@InProceedings{McEwan06,
title = "{A} {C}ircus {D}evelopment and {V}erification of an {I}nternet {P}acket {F}ilter.",
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
author= "McEwan, Alistair A.",
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
editor= "Welch, Peter H. and Kerridge, Jon and Barnes, Frederick R. M.",
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
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."
}