Formal verification
From Free net encyclopedia
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods.
As opposed to formal verification, Software testing cannot prove that a system does not have a certain defect and it cannot prove either that it does have a certain property. Only the process of formal verification can prove that a system does not have a certain defect or does have a certain property. Either way it is impossible to prove or test that a system has "no defect" since it is impossible to formally specify what "no defect" means. All we can do is prove that a system does not have any of the defects that we can think of, and has all of the properties that together make it functional and useful.
Formal verification can be used for example for systems such as cryptographic protocols, combinatorial circuits, digital circuits with internal memory, and software expressed as source code.
The verification of these systems is done by providing a formal proof on an abstract mathematical model of the system, the correspondance between the mathematical model and the nature of the system being otherwise known by construction. Examples of mathematical objects often used to model systems are : finite state machines, labelled transition systems, Petri nets, timed automata, hybrid automata, process algebra, formal semantics of programming languages such as operational semantics, denotational semantics, Hoare's logic.
There are roughly two approaches to formal verification. The first approach is model checking, which consists in a systematics and always automatic exploration of all the mathematical model, which then has to be of a finite nature. Usually this consists into exploring all of states and transitions in the model, by using smart and domain-specific abstraction techniques to consider whole bunches of states in a single operation and reduce computing time. Implementation techniques include state space enumeration, symbolic state space enumeration, abstract interpretation, abstraction refinement.
The second approach is logical inference. It consists in using a formal version of mathematical reasonning about the system, usually using theorem proving sofware such as the HOL theorem prover or Isabelle theorem prover. This is usually only partially automated and is driven by the user's understanding of the system to validate.
The properties to be verified are often described in temporal logics, such as linear temporal logic (LTL) or computational tree logic (CTL).
Validation and Verification
Verification is one aspect of testing a product's fitness for purpose. Validation is the complementary aspect. Often one refers to the overall checking process as V & V.
Validation: "Are we building the right product?", i.e., does the product do what the user really requires.
Verification: "Are we building the product right?", i.e., does the product conform to the specifications.
The verification process consists of static and dynamic parts. E.g., for a software product one can inspect the source code (static) and run against specific test cases (dynamic).
Validation usually can only be done dynamically, i.e., the product is tested by putting it through typical usages and atypical usages ("Can we break it?").
See also
- Important publications in formal verification
- Scalable Program Analysis
- Specification patterns for finite-state verification
- Formal equivalence checking
- Temporal logic in finite-state verification
- LURCH
- Property Specification LanguageTemplate:Soft-eng-stub
de:Verifizierung no:Verifikasjon ru:Верификация sk:Verifikácia uk:Верифікація