Formal specification
Encyclopedia
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 (necessarily) how the system should do it. Given such a specification, it is possible to use formal verification
techniques to demonstrate that a candidate system design is correct with respect to the specification. This has the advantage that incorrect candidate system designs can be revised before a major investment has been made in actually implementing the design. An alternative approach is to use provably correct refinement steps to transform a specification into a design, and ultimately into an actual implementation, that is correct by construction.
A design (or implementation) cannot ever be declared “correct” in isolation, but only “correct with respect to a given specification”. Whether the formal specification correctly describes the problem to be solved is a separate issue. It is also a difficult issue to address, since it ultimately concerns the problem constructing abstracted formal representations of an informal concrete problem domain
, and such an abstraction step is not amenable to formal proof. However, it is possible to validate
a specification by proving “challenge” theorem
s concerning properties that the specification is expected to exhibit. If correct, these theorems reinforce the specifier's understanding of the specification and its relationship with the underlying problem domain. If not, the specification probably needs to be changed to better reflect the domain understanding of those involved with producing (and implementing) the specification.
The Z notation
is an example of a leading formal specification language
. Others include the Specification Language(VDM-SL) of the Vienna Development Method
and the Abstract Machine Notation
(AMN) of the B-Method
. In the Web services area, formal specification is often used to describe non-functional properties (Web services Quality of Service
).
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...
, a formal specification is a mathematical
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
description of software or 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....
that may be used to develop an implementation
Implementation
Implementation is the realization of an application, or execution of a plan, idea, model, design, specification, standard, algorithm, or policy.-Computer Science:...
. It describes what the system should do, not (necessarily) how the system should do it. Given such a specification, it is possible to use 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...
techniques to demonstrate that a candidate system design is correct with respect to the specification. This has the advantage that incorrect candidate system designs can be revised before a major investment has been made in actually implementing the design. An alternative approach is to use provably correct refinement steps to transform a specification into a design, and ultimately into an actual implementation, that is correct by construction.
A design (or implementation) cannot ever be declared “correct” in isolation, but only “correct with respect to a given specification”. Whether the formal specification correctly describes the problem to be solved is a separate issue. It is also a difficult issue to address, since it ultimately concerns the problem constructing abstracted formal representations of an informal concrete problem domain
Problem domain
A problem domain is the area of expertise or application that needs to be examined to solve a problem. A problem domain is simply looking at only the topics you are interested in, and excluding everything else. For example, if you were developing a system trying to measure good practice in...
, and such an abstraction step is not amenable to formal proof. However, it is possible to validate
Verification and Validation
In software project management, software testing, and software engineering, verification and validation is the process of checking that a software system meets specifications and that it fulfills its intended purpose...
a specification by proving “challenge” theorem
Theorem
In mathematics, a theorem is a statement that has been proven on the basis of previously established statements, such as other theorems, and previously accepted statements, such as axioms...
s concerning properties that the specification is expected to exhibit. If correct, these theorems reinforce the specifier's understanding of the specification and its relationship with the underlying problem domain. If not, the specification probably needs to be changed to better reflect the domain understanding of those involved with producing (and implementing) the specification.
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:...
is an example of a leading formal specification language
Specification language
A 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...
. Others include the Specification Language(VDM-SL) of the Vienna Development Method
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...
and the Abstract Machine Notation
Abstract Machine Notation
The abstract machine notation is a specification language and programming language for specifying abstract machines in the B method, based on the mathematical theory of generalised substitutions....
(AMN) of the B-Method
B-Method
The 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...
. In the Web services area, formal specification is often used to describe non-functional properties (Web services Quality of Service
Quality of service
The quality of service refers to several related aspects of telephony and computer networks that allow the transport of traffic with special requirements...
).
See also
- Algebraic specificationAlgebraic specificationAlgebraic specification, is a software engineering technique for formally specifying system behavior. Algebraic specification seeks to systematically develop more efficient programs by:...
- Formal methodsFormal methodsIn 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...
- Specification (technical standard)Specification (technical standard)A specification is an explicit set of requirements to be satisfied by a material, product, or service. Should a material, product or service fail to meet one or more of the applicable specifications, it may be referred to as being out of specification;the abbreviation OOS may also be used...
- 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...
- 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...
External Links
- A Case for Formal Specification (Technology) by Coryoth 2005-07-30
- Formal Specification