Formal methods
Encyclopedia
In computer science
and software engineering
, formal methods are a particular kind of mathematically-based techniques for the specification
, development and verification
of software and hardware
systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design. However, the high cost of using formal methods means that they are usually only used in the development of high-integrity systems, where safety
or security
is of utmost importance.
Formal methods are best described as the application of a fairly broad variety of theoretical computer science
fundamentals, in particular logic calculi, formal language
s, automata theory, and program semantics, but also type systems and algebraic data types to problems in software and hardware specification and verification.
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).
Further information on this is expanded below.
As with programming language semantics
, styles of formal methods may be roughly classified as follows:
object modelling notation, Denney's synthesis of some aspects of the Z notation
with use case
driven development, and the CSK VDM
Tools.
.
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.
during the design
process (i.e., realized typically in software, but also potentially in hardware). For example:
properties of the specification (and hopefully by inference the developed system).
: 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.
Neither of these techniques work without human assistance. Automated theorem provers usually require guidance as to which properties are "interesting" enough to pursue; 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 oracle
s: 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.
, undetected errors may cause death
, so formal methods are more popular in this field than in other application areas.
Specification languages
Model checkers
Formal methods people
Software engineering disasters
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
and software engineering
Software engineering
Software Engineering is the application of a systematic, disciplined, quantifiable approach to the development, operation, and maintenance of software, and the study of these approaches; that is, the application of engineering to software...
, formal methods are a particular kind of mathematically-based techniques for the specification
Formal specification
In computer science, a formal specification is a mathematical description of software or hardware that may be used to develop an implementation. It describes what the system should do, not how the system should do it...
, development and verification
Formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics .- Usage :Formal verification can be...
of software and hardware
Hardware
Hardware is a general term for equipment such as keys, locks, hinges, latches, handles, wire, chains, plumbing supplies, tools, utensils, cutlery and machine parts. Household hardware is typically sold in hardware stores....
systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design. However, the high cost of using formal methods means that they are usually only used in the development of high-integrity systems, where safety
Safety
Safety is the state of being "safe" , the condition of being protected against physical, social, spiritual, financial, political, emotional, occupational, psychological, educational or other types or consequences of failure, damage, error, accidents, harm or any other event which could be...
or security
Security
Security is the degree of protection against danger, damage, loss, and crime. Security as a form of protection are structures and processes that provide or improve security as a condition. The Institute for Security and Open Methodologies in the OSSTMM 3 defines security as "a form of protection...
is of utmost importance.
Formal methods are best described as the application of a fairly broad variety of theoretical computer science
Theoretical computer science
Theoretical computer science is a division or subset of general computer science and mathematics which focuses on more abstract or mathematical aspects of computing....
fundamentals, in particular logic calculi, formal language
Formal language
A formal language is a set of words—that is, finite strings of letters, symbols, or tokens that are defined in the language. The set from which these letters are taken is the alphabet over which the language is defined. A formal language is often defined by means of a formal grammar...
s, automata theory, and program semantics, but also type systems and algebraic data types to problems in software and hardware specification and verification.
Taxonomy
Formal methods can be used at a number of levels:Level 0: Formal specification
Formal specification
In computer science, a formal specification is a mathematical description of software or hardware that may be used to develop an implementation. It describes what the system should do, not how the system should do it...
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
Formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics .- Usage :Formal verification can be...
may be used to produce a program in a more formal manner. For example, proofs of properties or refinement from the specification
Formal specification
In computer science, a formal specification is a mathematical description of software or hardware that may be used to develop an implementation. It describes what the system should do, not how the system should do it...
to a program may be undertaken. This may be most appropriate in high-integrity systems involving safety
Safety
Safety is the state of being "safe" , the condition of being protected against physical, social, spiritual, financial, political, emotional, occupational, psychological, educational or other types or consequences of failure, damage, error, accidents, harm or any other event which could be...
or security
Security
Security is the degree of protection against danger, damage, loss, and crime. Security as a form of protection are structures and processes that provide or improve security as a condition. The Institute for Security and Open Methodologies in the OSSTMM 3 defines security as "a form of protection...
.
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).
Further information on this is expanded below.
As with programming language semantics
Formal semantics of programming languages
In programming language theory, semantics is the field concerned with the rigorous mathematical study of the meaning of programming languages and models of computation...
, styles of formal methods may be roughly classified as follows:
- Denotational semanticsDenotational semanticsIn computer science, denotational semantics is an approach to formalizing the meanings of programming languages by constructing mathematical objects which describe the meanings of expressions from the languages...
, in which the meaning of a system is expressed in the mathematical theory of domainsDomain theoryDomain theory is a branch of mathematics that studies special kinds of partially ordered sets commonly called domains. Consequently, domain theory can be considered as a branch of order theory. The field has major applications in computer science, where it is used to specify denotational...
. 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 semanticsOperational semanticsIn computer science, operational semantics is a way to give meaning to computer programs in a mathematically rigorous way. Operational semantics are classified into two categories: structural operational semantics formally describe how the individual steps of a computation take place in a...
, 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 semanticsAxiomatic semanticsAxiomatic semantics is an approach based on mathematical logic to proving the correctness of computer programs. It is closely related to Hoare logic....
, in which the meaning of the system is expressed in terms of preconditionPreconditionIn computer programming, a precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification....
s and postconditionPostconditionIn computer programming, a postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification. Postconditions are sometimes tested using assertions within the code itself...
s which are true before and after the system performs a task, respectively. Proponents note the connection to classical logicLogicIn philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
; 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 AlloyAlloy language
In computer science and software engineering, the Alloy Analyzer is a software tool which can be used to analyze specifications written in the Alloy specification language. The Analyzer can generate instances of model invariants, simulate the execution of operations defined as part of the model,...
object modelling notation, Denney's synthesis of some aspects of the Z notation
Z notation
The Z notation , named after Zermelo–Fraenkel set theory, is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general.-History:...
with use case
Use case
In software engineering and systems engineering, a use case is a description of steps or actions between a user and a software system which leads the user towards something useful...
driven development, and the CSK VDM
Vienna Development Method
The Vienna Development Method is one of the longest-established Formal Methods for the development of computer-based systems. Originating in work done at IBM's Vienna Laboratory in the 1970s, it has grown to include a group of techniques and tools based on a formal specification language - the VDM...
Tools.
Uses
Formal methods can be applied at various points through the development processSoftware development process
A software development process, also known as a software development life cycle , is a structure imposed on the development of a software product. Similar terms include software life cycle and software process. It is often considered a subset of systems development life cycle...
.
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.The need for formal specification systems has been noted for years. In the ALGOL 58
ALGOL 58
ALGOL 58, originally known as IAL, is one of the family of ALGOL computer programming languages. It was an early compromise design soon superseded by ALGOL 60...
report, John Backus
John Backus
John Warner Backus was an American computer scientist. He directed the team that invented the first widely used high-level programming language and was the inventor of the Backus-Naur form , the almost universally used notation to define formal language syntax.He also did research in...
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
Once a formal specification has been produced, the specification may be used as a guide while the concrete system is developedSoftware development
Software development is the development of a software product...
during the design
Software design
Software design is a process of problem solving and planning for a software solution. After the purpose and specifications of software are determined, software developers will design or employ designers to develop a plan for a solution...
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 assertionAssertion (computing)In computer programming, an assertion is a predicate placed in a program to indicate that the developer thinks that the predicate is always true at that place.For example, the following code contains two assertions:...
s in the executable code.
Verification
Once a formal specification has been developed, the specification may be used as the basis for provingMathematical proof
In mathematics, a proof is a convincing demonstration that some mathematical statement is necessarily true. Proofs are obtained from deductive reasoning, rather than from inductive or empirical arguments. That is, a proof must demonstrate that a statement is true in all cases, without a single...
properties of the specification (and hopefully by inference the developed system).
Human-directed proof
Sometimes, the motivation for proving the correctness of a system is not the obvious need for re-assurance 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 proofMathematical proof
In mathematics, a proof is a convincing demonstration that some mathematical statement is necessarily true. Proofs are obtained from deductive reasoning, rather than from inductive or empirical arguments. That is, a proof must demonstrate that a statement is true in all cases, without a single...
: handwritten (or typeset) using natural language
Natural language
In the philosophy of language, a natural language is any language which arises in an unpremeditated fashion as the result of the innate facility for language possessed by the human intellect. A natural language is typically used for communication, and may be spoken, signed, or written...
, 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
Ambiguity
Ambiguity of words or phrases is the ability to express more than one interpretation. It is distinct from vagueness, which is a statement about the lack of precision contained or available in the information.Context may play a role in resolving 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 two general categories:- Automated theorem provingAutomated theorem provingAutomated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
, 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 checkingModel checkingIn computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
, 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.
Neither of these techniques work without human assistance. Automated theorem provers usually require guidance as to which properties are "interesting" enough to pursue; 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 oracle
Oracle machine
In complexity theory and computability theory, an oracle machine is an abstract machine used to study decision problems. It can be visualized as a Turing machine with a black box, called an oracle, which is able to decide certain decision problems in a single operation. The problem can be of any...
s: they make a pronouncement of truth, yet give no explanation of that truth. There is also the problem of "verifying the verifier
Quis custodiet ipsos custodes?
' is a Latin phrase traditionally attributed to the Roman poet Juvenal from his Satires , which is literally translated as "Who will guard the guards themselves?" Also sometimes rendered as "Who watches the watchmen?", the phrase has other idiomatic translations and adaptations such as "Who will...
"; 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.
Criticisms
The field of formal methods has its critics. Handwritten proofs of correctness need significant time (and thus money) to produce, with limited utility other than assuring correctness. This makes formal methods more likely to be used in fields where it is possible to perform automated proofs using software, or in cases where the cost of a fault is high. Example: in railway engineering and aerospace engineeringAerospace engineering
Aerospace engineering is the primary branch of engineering concerned with the design, construction and science of aircraft and spacecraft. It is divided into two major and overlapping branches: aeronautical engineering and astronautical engineering...
, undetected errors may cause death
Death
Death is the permanent termination of the biological functions that sustain a living organism. Phenomena which commonly bring about death include old age, predation, malnutrition, disease, and accidents or trauma resulting in terminal injury....
, so formal methods are more popular in this field than in other application areas.
Formal methods and notations
There are a variety of formal methods and notations available.Specification languages
- Abstract State MachinesAbstract State MachinesIn computer science, an abstract state machine is a state machine operating on states which are arbitrary data structures .The ASM Method is a practical and scientifically well-founded systems engineering method which bridges...
(ASMs) - ANSI/ISO C Specification LanguageANSI/ISO C Specification LanguageThe ANSI/ISO C Specification Language is a specification language for C programs, using Hoare style pre- and postconditions and invariants, that follows the design by contract paradigm...
(ACSL) - AlloyAlloy languageIn computer science and software engineering, the Alloy Analyzer is a software tool which can be used to analyze specifications written in the Alloy specification language. The Analyzer can generate instances of model invariants, simulate the execution of operations defined as part of the model,...
- B-MethodB-MethodThe B method is method of software development based on B, a tool-supported formal method based around an abstract machine notation, used in the development of computer software. It was originally developed by Jean-Raymond Abrial in France and the UK. B is related to the Z notation and supports...
- CADP
- Common Algebraic Specification LanguageCommon Algebraic Specification LanguageThe Common Algebraic Specification Language is a general-purpose specification languagebased on first-order logic with induction. Partial functionsand subsorting are also supported....
(CASL) - Process calculi
- CSPCommunicating sequential processesIn computer science, Communicating Sequential Processes is a formal language for describing patterns of interaction in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi...
- LOTOSLanguage Of Temporal Ordering SpecificationLanguage Of Temporal Ordering Specification is a formal specification language based on temporal ordering used for protocol specification in ISO OSI standards....
- π-calculusPi-calculusIn theoretical computer science, the π-calculus is a process calculus originally developed by Robin Milner, and David Walker as a continuation of work on the process calculus CCS...
- CSP
- Actor modelActor modelIn computer science, the Actor model is a mathematical model of concurrent computation that treats "actors" as the universal primitives of concurrent digital computation: in response to a message that it receives, an actor can make local decisions, create more actors, send more messages, and...
- EsterelEsterelEsterel is a synchronous programming language for the development of complex reactive systems. The imperative programming style of Esterel allows the simple expression of parallelism and preemption...
- LustreLustre programming languageLustre is a formally defined, declarative, and synchronous dataflow programming language for programming reactive systems. It began as a research project in the early 1980s. In 1993 it progressed to practical, industrial use in a commercial product as the core language of the industrial environment...
- mCRL2MCRL2mCRL2 is a specification language for describing concurrent discrete event systems. It is accompanied with a toolset, that facilitates tools, techniques and methods for simulation, analysis and visualization of behaviour. The behavioural part of the language is based on process algebra...
- Petri nets
- RAISERAISE specification languageRAISE was developed as part of the European ESPRIT II LaCoS project in the 1990s, led by Dines Bjørner. It consists of a set of tools based around a specification language for software development...
- Specification and Description LanguageSpecification and Description LanguageSpecification and Description Language is a specification language targeted at the unambiguous specification and description of the behaviour of reactive and distributed systems.- Overview :It is defined by the ITU-T...
- Temporal logic of actionsTemporal Logic of ActionsTemporal logic of actions is a logic developed by Leslie Lamport, which combines temporal logic with a logic of actions.It is used to describe behaviours of concurrent systems.- Details :...
(TLA) - USLUniversal Systems LanguageUnlike traditional languages, the Universal Systems Language is based on a preventative instead of a curative paradigm. Based on systems theory, to a great extent derived from lessons learned from the Apollo onboard flight software effort, USL has evolved over several decades and taken on multiple...
- VDMVienna Development MethodThe Vienna Development Method is one of the longest-established Formal Methods for the development of computer-based systems. Originating in work done at IBM's Vienna Laboratory in the 1970s, it has grown to include a group of techniques and tools based on a formal specification language - the VDM...
- VDM-SL
- VDM++
- Z notationZ notationThe Z notation , named after Zermelo–Fraenkel set theory, is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general.-History:...
- Rebeca Modeling LanguageRebeca Modeling LanguageRebeca is an actor-based modeling language with a formal foundation, designed in an effort to bridge the gap between formal verification approaches and real applications. It can be considered as a reference model for concurrent computation, based on an operational interpretation of the actor model...
Model checkers
- SPINSPIN model checkerSPIN is a general tool for verifying the correctness of distributed software models in a rigorous and mostly automated fashion. It was written by Gerard J. Holzmann and others in the original Unix group of the Computing Sciences Research Center at Bell Labs, beginning in 1980...
- PAT is a powerful free model checker, simulator and refinement checker for concurrent systems and CSP extensions (e.g. shared variables, arrays, fairness).
See also
- Automated theorem provingAutomated theorem provingAutomated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
- Design by contractDesign by contractDesign by contract , also known as programming by contract and design-by-contract programming, is an approach to designing computer software...
Formal methods people
- Formal specificationFormal specificationIn computer science, a formal specification is a mathematical description of software or hardware that may be used to develop an implementation. It describes what the system should do, not how the system should do it...
- Formal verificationFormal verificationIn the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics .- Usage :Formal verification can be...
- Formal systemFormal systemIn formal logic, a formal system consists of a formal language and a set of inference rules, used to derive an expression from one or more other premises that are antecedently supposed or derived . The axioms and rules may be called a deductive apparatus...
- Model checkingModel checkingIn computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
- Software engineeringSoftware engineeringSoftware Engineering is the application of a systematic, disciplined, quantifiable approach to the development, operation, and maintenance of software, and the study of these approaches; that is, the application of engineering to software...
Software engineering disasters
- Specification languageSpecification languageA specification language is a formal language used in computer science.Unlike most programming languages, which are directly executable formal languages used to implement a system, specification languages are used during systems analysis, requirements analysis and systems design.Specification...