An Overview of the Verification of a Handel-C Program

Woodcock, Jim and McEwan, Alistair A. (2000) An Overview of the Verification of a Handel-C Program. In: International Conference on Parallel and Distributed Processing Techniques and Applications, Jun 26-29, 2000, Las Vegas, NV, . (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided)

The full text of this publication is not available from this repository. (Contact us about this Publication)


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

Item Type: Conference or workshop item (Paper)
Uncontrolled keywords: Handel-C; hardware verification; abstraction; model checking; data refinement; the Unifying Theory of Programming; Z; CSP; FDR; Z/Eves
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Systems Architecture Group
Depositing User: Mark Wheadon
Date Deposited: 01 Oct 2009 19:34
Last Modified: 15 Jul 2014 09:10
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):