Date of this Version

July 2002

Document Type

Conference Proceeding

Publication Details

Padmanabhan Krishnan and Danita Hartley (2002) Using model checking to test a firewall : A case study. In: Proceedings of the Euromicro Conference: Software Process and Product Improvement, pp 284-293, Dortmund, Germany, 2002.
Copyright © IEEE 2002.

Published by the Institute of Electrical and Electronics Engineers (IEEE)
Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.


This paper summarises our experience in using model checking technology to test concurrent programs. We use the tool Verisoft to understand various aspects of a firewall tool kit by instrumenting three components of the firewall tool kit with hooks to test their behaviour. Some of the key changes include changing socket communication to message passing queues and adding appropriate synchronisations so that the behaviour of the system can be tracked. We aim to minimize the number of changes to the original source code so that its original behaviour is not affected. The main conclusion is that it is possible to inspect source code with a view towards verifying key behavioural properties without understanding the entire behaviour of the system.



This document has been peer reviewed.