Overview of formal methods in software engineering

The most common way to check for faults and bugs in IT systems is to use testing, simulations and human reviews. Nevertheless, these techniques are not exhaustive and cannot guarantee the absence of defects. A more promising method is to use formal methods during the development process of the IT system, for example by writing a formal specification of the system on which different properties can be proved and then mathematically proving that the implementation of the system abides by the specification. In this report we aim to give a brief introduction to the field of formal methods together with a classification of the different existing formal methods. We also guide the reader through some of the existing literature in the field and we present some systems where formal methods are used to prove security properties. An overview of a functional correctness proof for a security-critical micro-kernel is also provided. From the literature we have surveyed we conclude that using formal methods can be cost-effective in the long run and it can reduce the number of defects to close to zero. Nevertheless, the methods are not yet widely used and, therefore, there are a limited number of tools that can be used.