Jump to content

Software verification

From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Jeanqasaur (talk | contribs) at 04:40, 13 September 2014 (→Static verification (Analysis)). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

Software verification is a discipline of software engineering whose goal is to assure that software fully satisfies all the expected requirements.

There are two fundamental approaches to verification:

  • Dynamic verification, also known as Test or Experimentation - This is good for finding bugs
  • Static verification, also known as Analysis - This is useful for proving correctness of a program although it may result in false positives

Dynamic verification (Test, experimentation)

Dynamic verification is performed during the execution of software, and dynamically checks its behaviour; it is commonly known as the Test phase. Verification is a Review Process. Depending on the scope of tests, we can categorize them in three families:

  • Test in the small: a test that checks a single function or class (Unit test)
  • Test in the large: a test that checks a group of classes, such as
    • Module test (a single module)
    • Integration test (more than one module)
    • System test (the entire system)
  • Acceptance test: a formal test defined to check acceptance criteria for a software
    • Functional test
    • Non functional test (performance, stress test)

Software verification is often confused with software validation. The difference between verification and validation:

  • Software verification asks the question, "Are we building the product right?"; that is, does the software conform to its specification.
  • Software validation asks the question, "Are we building the right product?"; that is, is the software doing what the user really requires.

The aim of software verification is to find the errors introduced by an activity, i.e. check if the product of the activity is as correct as it was at the beginning of the activity.

Static verification (Analysis)

Static verification is the process of checking that software meets requirements by inspecting the code before it runs. For example:

Verification by Analysis - The analysis verification method applies to verification by investigation, mathematical calculations, logical evaluation, and calculations using classical textbook methods or accepted general use computer methods. Analysis includes sampling and correlating measured data and observed test results with calculated expected values to establish conformance with requirements.

Formal Verification

Formal verification of software programs involves proving that a program satisfies a formal specification of its behavior. Subareas of formal verification include abstract interpretation, automated theorem proving, type systems, and lightweight formal methods.

These techniques can be sound, meaning that the verified properties can be logically deduced from the semantics, or unsound, meaning that there is no such guarantee. A sound technique yields a result only once it has searched the entire space of possibilities. An example of an unsound technique is one that searches only a subset of the possibilities, for instance only integers up to a certain number, and give a "good-enough" result. We also talk about whether these techniques are decidable, whether they are guaranteed to terminate with an answer. Because they are bounded, unsound techniques are often more likely to be decidable than sound ones.

See also

References

Retrieved from "https://en.wikipedia.org/w/index.php?title=Software_verification&oldid=625331069"