The What, How, and When of Formal Methods

Introduction

Formal Methods (FM) is an area of Software Engineering. They comprise a collection of methodologies and related tools, employing a mathematical basis –as do most engineering disciplines–, to construct its products. Although FM are part of Software Engineering, they extend their scope to the development not only of software products but also of hardware systems.

The goal of this article is to give answers to questions such as what are Formal Methods, how are Formal Methods implemented, how are they used in Software Engineering, when should they be used, among other related questions.

The chapter starts answering the question of what are FM; also the aims of FM are stated at the same time that their main characteristics are presented.

An example that shows how FM can be used to help specifying software requirements as well as the rest of the stages in a software development process is given as answers to the questions how are FM implemented and how FM are used in Software Engineering.

A discussion about when they should be used, explaining why they should be employed when the software system is required to be as secure and reliable as possible and how they can also be used as a complement to traditional development methods, is also provided.

A section on the state of the art in FM, providing an analysis of Lightweight FM and the growing impact that Model Checking is having in the software and hardware industry as an automatic FM for system verification, is presented. Finally, a discussion on the use of automatic analyzers like Alloy, which replace conventional analysis based in theorem proof by a “non-complete” analysis based in the examination of cases, is also given.