Formal Methods Overview

Formal Methods Overview

Ana Funes (Universidad Nacional de San Luis, Argentina) and Aristides Dasso (Universidad Nacional de San Luis, Argentina)
Copyright: © 2015 |Pages: 10
DOI: 10.4018/978-1-4666-5888-2.ch704

Chapter Preview


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


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.

Table 1.
A synoptic view of formal methods, formal systems and formal languages
Formal MethodFormal SystemFormal NotationFormal Language: formal syntax + formal semantics.
Proof system: axioms + inference rules
Automatic tool support for specification, proof assistance, code generation, etc.

Key Terms in this Chapter

Semantics: In a language, the meaning of a string, as opposed to syntax, which describes how the symbols of the language are combined. Most programming languages have their syntax defined formally (traditionally in BNF), while formal specification languages have also their semantics defined formally.

Verification: The process of determining whether or not the products of a specification phase fulfill a set of established requirements. Sometimes this is also used to indicate the process of proving that a more concrete specification preserved the properties of a more abstract specification.

Specification: A document describing what a system should do, what a problem is or what a domain is all about. In formal methods this document is written in a formal language.

Complete Chapter List

Search this Book: