This article needs additional citations for verification. Please help improve this article by adding reliable references. Unsourced material may be challenged and removed. (June 2009)

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^{[citation needed]}.

[edit] Usage

Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational 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 correspondence 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, axiomatic semantics and Hoare logic.^{[citation needed]}

[edit] Approaches to formal verification

There are roughly two approaches to formal verification.^{[citation needed]}

The first approach is model checking, which consists of a systematically exhaustive exploration of the mathematical model (this is possible for finite models, but also for some infinite models where infinite sets of states can be effectively represented). Usually this consists of exploring all states and transitions in the model, by using smart and domain-specific abstraction techniques to consider whole groups of states in a single operation and reduce computing time. Implementation techniques include state space enumeration, symbolic state space enumeration, abstract interpretation, symbolic simulation, abstraction refinement. The properties to be verified are often described in temporal logics, such as linear temporal logic (LTL) or computational tree logic (CTL).

The second approach is logical inference. It consists of using a formal version of mathematical reasoning about the system, usually using theorem proving software such as a HOL theorem prover, the ACL2, Isabelle, or Coq theorem provers. This is usually only partially automated and is driven by the user's understanding of the system to validate.

[edit] Validation and Verification

It has been suggested that this article or section be merged into Verification and Validation#Terminology . (Discuss)

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 trying to make the right thing?", i.e., is the product specified to the user's actual needs?
• Verification: "Have we made what we were trying to make?", i.e., does the product conform to the specifications?

The verification process consists of static/structural and dynamic/behavioral aspects. E.g., for a software product one can inspect the source code (static) and run against specific test cases (dynamic). Validation usually can be done only dynamically, i.e., the product is tested by putting it through typical and atypical usages ("Does it satisfactorily meet all use cases?"). See also Verification and Validation

[edit] Industry usage

The growth in complexity of designs increases the importance of formal verification techniques in the hardware industry.^[1][2] At present, formal verification is used by most or all leading hardware companies, but its use in the software industry is still languishing. This could be attributed to the greater need in the hardware industry, where errors have greater commercial significance. Because of the potential subtle interactions between components, it is increasingly difficult to exercise a realistic set of possibilities by simulation. Important aspects of hardware design are amenable to automated proof methods, making formal verification easier to introduce and more productive.^[3]

As of 2009^[update], only two operating systems have been formally verified: NICTA's Secure Embedded L4 microkernel, and Green Hills Software's Integrity operating system.^[4]

[edit] See also

Software Testing portal

Look up verifiability in Wiktionary, the free dictionary.

• Automated theorem proving
• Formal equivalence checking
• LURCH
• Model checking
• Proof checker
• Property Specification Language
• Selected formal verification bibliography
• Static code analysis
• Temporal logic in finite-state verification
• Post silicon validation
• Intelligent verification
• Verification and Validation
• Runtime verification

[edit] References