From TheBestLinks.com
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.
System types that are considered in the literature for formal verification
include finite state machines (FSM),
labelled transition systems (LTS) and
their compositions,
Petri nets, timed automata and hybrid automata,
cryptographic protocols,
combinatorial circuits,
digital circuits with internal memory,
and abstractions of general software components.
The properties to be verified are often described
in temporal logics, such as linear-time temporal logic (LTL) or computational tree logic (CTL).
Usually formal verification is carried out algorithmically.
The main approaches to implementing formal verification
include state space enumeration, symbolic state space enumeration, abstract interpretation,
abstraction refinement, process-algebraic methods,
and reasoning with the aid of automatic theorem provers such as
HOL or Isabelle.
See also
Related links
Top visited
0 of
0 links
[no links posted yet]
>> place link >>
Discussion
Last posted
0 of
0 messages
[no messages posted yet]
>> post message >>
Watch
You can
add this article to your own "watchlist" and receive e-mail notification about all changes in this page.
