The What, How, and When of Formal Methods

The What, How, and When of Formal Methods

Aristides Dasso (Universidad Nacional de San Luis, Argentina) and Ana Funes (Universidad Nacional de San Luis, Argentina)
Copyright: © 2018 |Pages: 13
DOI: 10.4018/978-1-5225-2255-3.ch662
OnDemand PDF Download:
$30.00
List Price: $37.50

Abstract

Questions such as what are Formal Methods, how are Formal Methods implemented, how are they used in Software Engineering and when should they be used, among other related questions, are the main objective of this article. Some definitions are given to answer some of these questions; the article also states the aims of FM as well as it gives their main characteristics. An example that shows how Formal Methods can be used for specifying not only software requirements but also the rest of the stages in a software development process is given. A discussion about when they should be used, explaining the reasons why they should be applied when security and reliability are important requirements of the software under development, is presented. Finally, some arguments about how they can also be used as a complement to traditional development methods are provided.
Chapter Preview
Top

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.

Key Terms in this Chapter

Proof System: Provides a way of deducing formulae, beginning with the axioms of the logic and using its rules of inference.

Verification: The process of determining whether a product fulfills a set of previously established requirements. In formal verification, this is the process of proving that a more concrete specification preserves 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 using a formal language.

Formal Proof: Finite sequence of well formed sentences of a formal language, where each sentence either is an axiom or it follows from the previous sentences derived using a rule of inference; the last sentence is the assertion to be proved (theorem).

Model-Based Specification: Formal specification using concrete types and explicit function definitions.

Property-Oriented Specification: Formal specification given in an abstract style, where the system behavior is defined by a set of properties. These properties are given by axioms relating functions and sorts. (See Algebraic Specification).

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

Complete Chapter List

Search this Book:
Reset