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.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com