Modelling and refinement of forensic data acquisition specifications

Benjamin Aziz

Research output: Contribution to journalArticlepeer-review

405 Downloads (Pure)


This paper defines a model of a special type of digital forensics tools, known as data acquisition tools, using the formal refinement language Event-B. The complexity and criticality of many types of computer and Cyber crime nowadays combined with improper or incorrect use of digital forensic tools calls for more robust and reliable specifications of the functionality of digital forensics applications. As a minimum, the evidence produced by such tools must meet the minimum admissibility standards the legal system requires, in general implying that it must be generated from reliable and robust tools. Despite the fact that some research and effort has been spent on the validation of digital forensics tools by means of testing, the verification of such tools and the formal specification of their expected behaviour remains largely under-researched. The goal of this work is to provide a formal specification against which implementations of data acquisition procedures can be analysed.
Original languageEnglish
Pages (from-to)90-101
JournalDigital Investigation
Issue number2
Early online date5 May 2014
Publication statusPublished - Jun 2014


  • Formal Specifications
  • Formal Refinement
  • Event-B Method
  • Disk Data Acquisition
  • Computer Forensics


Dive into the research topics of 'Modelling and refinement of forensic data acquisition specifications'. Together they form a unique fingerprint.

Cite this