Formal Methods Overview

2. Background

Formal Methods (FM) cover a wide range of methodologies that employ mathematical tools in Software Engineering. FM are a collection of methodologies and related tools, geared to the production of software employing a mathematical basis. There are a number of different FM each having its own methodology and tools, specially a formal specification language.

Hinchey and Bowen (1995) establish that “Formal Methods allow us to propose properties of the system and to demonstrate that they hold. They make it possible for us to examine system behavior and to convince ourselves that all possibilities have been anticipated. Finally they enable us to prove the conformance of an implementation with its specification.”

Most FM are based mainly on the use of formal specifications –for which they normally have a language to express them– and the possibility of achieving formal verification of all or part of the developed software. Sometimes they propose also a process to be followed using a formal language during software development as well as other tools for verification such as an assisted prover or a model checker.

The aims of FM can vary according to the different methodologies they support, but they all share a common goal: the production of software with the utmost quality. To achieve this, different FM have developed not only a theory but also different tools to support their respective formal processes. The existence of a large and growing number of languages, methods and tools that promote the application of formal specifications shows the growing interest in this area (see http://formalmethods.wikia.com/wiki/Formal_methods).

3. Formal Languages, Systems, And Methods

There is some confusion in the use of terms formal language, formal notation, formal system and formal method. Alagar and Periyasamy (2011) make clear the differences among a formal language, a formal system and a formal method (see Table 1). According to them, a formal notation or language is a language that has both its syntax and semantics formally defined.