An overview of the verification of a Handel-C program

In this short paper we describe the verification of a Handel-C program that implements a packet-filter firewall on an FPGA. The Handel-C program is modelled as a system of co-operating CSP processes; unfortunately, the system is too large to be subjected to model checking (it is of the order of 10(50) states). A series of reductions is used to produce an abstract system that approximates the behaviour of the Handel-C program; this abstract system is small enough to be model-checked by FDR, yet exact with respect to critical system properties. The exactness of the abstraction is justified by the principles of data refinement. The most abstract description is given using Hoare & He's Unifying Theory.