Using model checking to test a firewall : A case study.Information Technology papers
Date of this Version7-1-2002
Document TypeConference Proceeding
AbstractThis 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.
Citation InformationPadmanabhan Krishnan and Danita Hartley. "Using model checking to test a firewall : A case study." (2002)
Available at: http://works.bepress.com/paddy_krishnan/8/