Formal methods are best described as the application of a fairly broad variety of theoretical computer science fundamentals, in particular logic calculi, formal languages, automata theory, discrete event dynamic system and program semantics, but also type systems and algebraic data types to problems in software and hardware specification and verification.
Background
Semi-Formal Methods are formalisms and languages that are not considered fully “formal”.
It defers the task of completing the semantics to a later stage, which
is then done either by human interpretation or by interpretation through
software like code or test case generators.
Taxonomy
Formal methods can be used at a number of levels:
Level 0: Formal specification may be undertaken and then a program developed from this informally. This has been dubbed formal methods lite. This may be the most cost-effective option in many cases.
Level 1: Formal development and formal verification may be used to produce a program in a more formal manner. For example, proofs of properties or refinement from the specification to a program may be undertaken. This may be most appropriate in high-integrity systems involving safety or security.
Level 2: Theorem provers
may be used to undertake fully formal machine-checked proofs. This can
be very expensive and is only practically worthwhile if the cost of
mistakes is extremely high (e.g., in critical parts of microprocessor
design).
- Denotational semantics, in which the meaning of a system is expressed in the mathematical theory of domains. Proponents of such methods rely on the well-understood nature of domains to give meaning to the system; critics point out that not every system may be intuitively or naturally viewed as a function.
- Operational semantics, in which the meaning of a system is expressed as a sequence of actions of a (presumably) simpler computational model. Proponents of such methods point to the simplicity of their models as a means to expressive clarity; critics counter that the problem of semantics has just been delayed (who defines the semantics of the simpler model?).
- Axiomatic semantics, in which the meaning of the system is expressed in terms of preconditions and postconditions which are true before and after the system performs a task, respectively. Proponents note the connection to classical logic; critics note that such semantics never really describe what a system does (merely what is true before and afterwards).
Lightweight formal methods
Some practitioners believe that the formal methods community has overemphasized full formalization of a specification or design.
They contend that the expressiveness of the languages involved, as well
as the complexity of the systems being modelled, make full
formalization a difficult and expensive task. As an alternative, various
lightweight formal methods, which emphasize partial
specification and focused application, have been proposed. Examples of
this lightweight approach to formal methods include the Alloy object modelling notation, Denney's synthesis of some aspects of the Z notation with use case driven development, and the CSK VDM Tools.
Uses
Formal methods can be applied at various points through the development process.
Specification
Formal
methods may be used to give a description of the system to be
developed, at whatever level(s) of detail desired. This formal
description can be used to guide further development activities (see
following sections); additionally, it can be used to verify that the
requirements for the system being developed have been completely and
accurately specified. or formalising system requirements by expressing
them in a formal language with a precise and unambiguously defined
syntax and semantics.
The need for formal specification systems has been noted for years. In the ALGOL 58 report, John Backus presented a formal notation for describing programming language syntax, later named Backus normal form then renamed Backus–Naur form (BNF).
Backus also wrote that a formal description of the meaning of
syntactically valid ALGOL programs wasn't completed in time for
inclusion in the report. "Therefore the formal treatment of the
semantics of legal programs will be included in a subsequent paper." It
never appeared.
Development
Formal development using formal methods as an integrated part of a tool-supported system development process.
Once a formal specification has been produced, the specification may be used as a guide while the concrete system is developed during the design process (i.e., realized typically in software, but also potentially in hardware). For example:
- If the formal specification is in an operational semantics, the observed behavior of the concrete system can be compared with the behavior of the specification (which itself should be executable or simulateable). Additionally, the operational commands of the specification may be amenable to direct translation into executable code.
- If the formal specification is in an axiomatic semantics, the preconditions and postconditions of the specification may become assertions in the executable code.
Verification
Formal
verification using a software tool to prove properties of a formal
specification, or that a formal model of a system implementation
satisfies its specification.
Once a formal specification has been developed, the specification may be used as the basis for proving properties of the specification (and hopefully by inference the developed system).
Sign-off verification
A
formal verification tool for sign-off verification is a tool that is
highly trusted such that it can replace traditional verification methods
(the tool may even be certified).
Human-directed proof
Sometimes, the motivation for proving the correctness
of a system is not the obvious need for reassurance of the correctness
of the system, but a desire to understand the system better.
Consequently, some proofs of correctness are produced in the style of mathematical proof: handwritten (or typeset) using natural language,
using a level of informality common to such proofs. A "good" proof is
one which is readable and understandable by other human readers.
Critics of such approaches point out that the ambiguity
inherent in natural language allows errors to be undetected in such
proofs; often, subtle errors can be present in the low-level details
typically overlooked by such proofs. Additionally, the work involved in
producing such a good proof requires a high level of mathematical
sophistication and expertise.
Automated proof
In
contrast, there is increasing interest in producing proofs of
correctness of such systems by automated means. Automated techniques
fall into three general categories:
- Automated theorem proving, in which a system attempts to produce a formal proof from scratch, given a description of the system, a set of logical axioms, and a set of inference rules.
- Model checking, in which a system verifies certain properties by means of an exhaustive search of all possible states that a system could enter during its execution.
- Abstract interpretation, in which a system verifies an over-approximation of a behavioural property of the program, using a fixpoint computation over a (possibly complete) lattice representing it.
Some automated theorem provers require guidance as to which
properties are "interesting" enough to pursue, while others work without
human intervention. Model checkers can quickly get bogged down in
checking millions of uninteresting states if not given a sufficiently
abstract model.
Proponents of such systems argue that the results have greater
mathematical certainty than human-produced proofs, since all the tedious
details have been algorithmically verified. The training required to
use such systems is also less than that required to produce good
mathematical proofs by hand, making the techniques accessible to a wider
variety of practitioners.
Critics note that some of those systems are like oracles: they make a pronouncement of truth, yet give no explanation of that truth. There is also the problem of "verifying the verifier";
if the program which aids in the verification is itself unproven, there
may be reason to doubt the soundness of the produced results. Some
modern model checking tools produce a "proof log" detailing each step in
their proof, making it possible to perform, given suitable tools,
independent verification.
The main feature of the abstract interpretation approach is that
it provides a sound analysis, i.e. no false negatives are returned.
Moreover, it is efficiently scalable, by tuning the abstract domain
representing the property to be analyzed, and by applying widening
operators to get fast convergence.
Applications
Formal
methods are applied in different areas of hardware and software,
including routers, Ethernet switches, routing protocols, and security
applications. There are several examples in which they have been used to
verify the functionality of the hardware and software used in DCs. IBM used ACL2, a theorem prover, in AMD x86 processor development process. Intel uses such methods to verify its hardware and firmware (permanent software programmed into a read-only memory). Dansk Datamatik Center used formal methods in the 1980s to develop a compiler system for the Ada programming language that went on to become a long-lived commercial product.
There are several other projects of NASA in which formal methods are applied, such as Next Generation Air Transportation System, Unmanned Aircraft System integration in National Airspace System, and Airborne Coordinated Conflict Resolution and Detection (ACCoRD).
B-Method with AtelierB, is used to develop safety automatisms for the various subways installed throughout the world by Alstom and Siemens, and also for Common Criteria certification and the development of system models by ATMEL and STMicroelectronics.
Formal verification has been frequently used in hardware by most
of the well-known hardware vendors, such as IBM, Intel, and AMD. There
are many areas of hardware, where Intel have used FMs to verify the
working of the products, such as parameterized verification of cache
coherent protocol, Intel Core i7 processor execution engine validation (using theorem proving, BDDs, and symbolic evaluation), optimization for Intel IA-64 architecture using HOL light theorem prover,
and verification of high performance dual-port gigabit Ethernet
controller with a support for PCI express protocol and Intel advance
management technology using Cadence. Similarly, IBM has used formal methods in the verification of power gates, registers, and functional verification of the IBM Power7 microprocessor.
In software development
In software development,
formal methods are mathematical approaches to solving software (and
hardware) problems at the requirements, specification, and design
levels. Formal methods are most likely to be applied to safety-critical
or security-critical software and systems, such as avionics software. Software safety assurance standards, such as DO-178C allows the usage of formal methods through supplementation, and Common Criteria mandates formal methods at the highest levels of categorization.
For sequential software, examples of formal methods include the B-Method, the specification languages used in automated theorem proving, RAISE, and the Z notation.
In functional programming, property-based testing
has allowed the mathematical specification and testing (if not
exhaustive testing) of the expected behaviour of individual functions.
The Object Constraint Language (and specializations such as Java Modeling Language) has allowed object-oriented systems to be formally specified, if not necessarily formally verified.
For concurrent software and systems, Petri nets, process algebra, and finite state machines (which are based on automata theory - see also virtual finite state machine or event driven finite state machine) allow executable software specification and can be used to build up and validate application behavior.
Another approach to formal methods in software development is to
write a specification in some form of logic—usually a variation of first-order logic (FOL)—and then to directly execute the logic as though it were a program. The OWL language, based on Description Logic
(DL), is an example. There is also work on mapping some version of
English (or another natural language) automatically to and from logic,
and executing the logic directly. Examples are Attempto Controlled English,
and Internet Business Logic, which do not seek to control the
vocabulary or syntax. A feature of systems that support bidirectional
English-logic mapping and direct execution of the logic is that they can
be made to explain their results, in English, at the business or
scientific level.
Formal methods and notations
There are a variety of formal methods and notations available.
Specification languages
- Abstract State Machines (ASMs)
- A Computational Logic for Applicative Common Lisp (ACL2)
- ANSI/ISO C Specification Language (ACSL)
- Alloy
- Autonomic System Specification Language (ASSL)
- B-Method
- CADP
- Common Algebraic Specification Language (CASL)
- Java Modeling Language (JML)
- Knowledge Based Software Assistant (KBSA)
- Process calculi
- Actor model
- Esterel
- Lustre
- mCRL2
- Perfect Developer
- Petri nets
- Predicative programming
- RAISE
- Rebeca Modeling Language
- SPARK Ada
- Spec sharp (Spec#)
- Specification and Description Language
- TLA+
- USL
- VDM
- VDM-SL
- VDM++
- Z notation
Model checkers
- SPIN
- PAT is a powerful free model checker, simulator and refinement checker for concurrent systems and CSP extensions (e.g. shared variables, arrays, fairness).
- MALPAS Software Static Analysis Toolset is an industrial strength model checker used for formal proof of safety-critical systems
- UPPAAL
- ESBMC
