Software verification: Difference between revisions

Revision as of 02:20, 19 July 2005

Latest revision as of 18:46, 23 June 2025

(118 intermediate revisions by 72 users not shown)

Line 1:

{{Short description|Verification that software meets requirements}}

'''Software verification''' is a broad and complex discipline of [[software engineering]], [[programming languages]], and [[theory of computation]] whose goal is to assure that a software fully satisfies all the expected requirements.

== Broad scope and classification ==

There are two fundamental approaches to verification:

* ''Dynamic verification'', also known as [[Test]] or [[Experimentation]]

* ''Static verification'', also known as [[Analysis]]

A broad definition of verification makes it related to [[software testing]]. In that case, there are two fundamental approaches to verification:

== Dynamic verification (Test, Experimentation) ==

* ''Dynamic verification'', also known as [[experimentation]], [[dynamic testing]] or, simply testing. - This is good for finding faults ([[software bugs]]).

* ''Static verification'', also known as [[static code analysis|analysis]] or, [[static code analysis|static testing]] - This is useful for proving the [[Correctness (computer science)|correctness]] of a program. Although it may result in false positives when there are one or more conflicts between the process a software really does and what the static verification assumes it does.

Under the [[ACM Computing Classification System]], software verification topics appear under "Software and its engineering", within "Software creation", whereas [[Program verification]] also appears under [[Theory of computation]] under Semantics and reasoning, Program reasoning.

Dynamic verification is performed during the execution of a software, and dynamically checks its behaviour; it is commonly known as [[Test]] phase.

== Dynamic verification (Test, Experimentationexperimentation) ==

Dynamic verification is performed during the execution of a software, and dynamically checks its behaviourbehavior; it is commonly known as the [[Software testing|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 checkchecks a single funtionfunction or class ([[Unit test]])

* ''Test in the large'': a test that checkchecks a group of classes, such as

** Module test (a single module)

** [[Integration test]] (more than one module)

Line 16 ⟶ 22:

* ''Acceptance test'': a formal test defined to check acceptance criteria for a software

** Functional test

** Non functional test (performance, [[stress testing (software)|stress test]])

The aim of software dynamic verification is to find the errors introduced by an activity (for example, having a medical software to analyze bio-chemical data); or by the repetitive performance of one or more activities (such as a stress test for a web server, i.e. check if the current product of the activity is as correct as it was at the beginning of the activity).

== Static verification (Analysis) ==

Static verification is athe process toof checkchecking somethat requirementssoftware ofmeets arequirements softwareby doinginspecting athe physicalcode inspectionbefore ofit itruns. For example:

* ''[[Code conventions]] verification''

* ''Bad practices ([[anti-pattern]]) detection''

* [[Software metric]]s calculation

* [[Formal verification#Formal verification for software|Formal verification]]

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.

== Narrow scope ==

When it is defined more strictly, verification is equivalent only to static testing and it is intended to be applied to artifacts. And, validation (of the whole software product) would be equivalent to dynamic testing and intended to be applied to the running software product (not its artifacts, except requirements). Notice that requirements validation can be performed statically and dynamically (See [[Software verification and validation#Artifact or specification validation|artifact validation]]).

== Comparison with validation ==

{{Main|Software verification and validation}}

Software verification is often confused with software validation. The difference between [[Verification and validation (software)|''verification'' and ''validation'']]:

* Software ''verification'' asks the question, "Are we building the product right?"; that is, does the software conform to its specifications? (As a house conforms to its blueprints.)

* Software ''validation'' asks the question, "Are we building the right product?"; that is, does the software do what the user really requires? (As a house conforms to what the owner needs and wants.)

==See also==

* [[Verification and validation (software)]]

* [[Runtime verification]]

* [[Hardware verification]]

* [[Formal verification]]

== References ==

* [[Carlo Ghezzi]], [[Mehdi Jazayeri]], [[Dino MandrioliIEEE]]: ''FundamentalsSWEBOK: ofGuide to the Software Engineering'', PrenticeBody Hall,of ISBN 013099183XKnowledge''

* [[Carlo Ghezzi]], [[Mehdi Jazayeri]], [[Dino Mandrioli]]: ''Fundamentals of Software Engineering'', Prentice Hall, {{ISBN|0-13-099183-X}}

* [[Alan L. Breitler]]: ''A Verification Procedure for Software Derived from Artificial Neural Networks'', Journal of the International Test and Evaluation Association, Jan 2004, Vol 25, No 4.

* Vijay D'Silva, [[Daniel Kroening]], Georg Weissenbacher: [http://www.kroening.com/papers/tcad-sw-2008.pdf A Survey of Automated Techniques for Formal Software Verification]. IEEE Trans. on CAD of Integrated Circuits and Systems 27(7): 1165-1178 (2008)

[[Category:Software testing]]