verification

from Wikipedia, the free encyclopedia

Verification or verification (from Latin veritas 'truth' and facere ' to make') is the proof that a suspected or alleged fact is true . The term is used differently, depending on whether the establishment of the truth can only be based on provided evidence or whether the more easily realizable confirmatory examination and certification of the facts through arguments from an independent body is considered verification.

Metrology

In the international dictionary of metrology (JCGM 200: 2012) verification is defined as follows: Verification is the provision of objective evidence that a unit under consideration meets the specified requirements. This is, for example, proof that the specified measurement uncertainty has been achieved in a measuring system.

Philosophy of science

In the theory of science , verification of a hypothesis is the proof that this hypothesis is correct. Logical empiricism and positivism assume that such evidence is feasible. In the context of critical rationalism ( Karl Popper ) it is argued that verification does not exist. General legal statements can only be true, but unverified, or they can be falsified with descriptions of facts that contradict the statements, i.e. they can be found to be invalid. To understand an example given by Karl Popper: Assuming the hypothesis is: "All swans are white", finding numerous white swans only helps to ensure that the hypothesis can be maintained. There is always the possibility of finding a different colored swan. If this occurs, the hypothesis is refuted. As long as no swan of a different color has been found, the hypothesis can still be regarded as not refuted - that is, as "validated".

Falsificationism also applies to localizing existence hypotheses (also called certain existence hypotheses): The (general) hypothesis “There are white swans” cannot be tested in isolation. However, if one has the whereabouts of a white swan in a space-time area, falsification is possible, and the easier the more restricted this area is. If there is no white swan there, the hypothesis can be considered refuted. Conversely, the unfalsifiable statement “There are white swans” follows from such a certain existence hypothesis as “On August 25th there is a white swan in the Augsburg Zoo”. However, it is not already verified by the fact that the falsification does not occur (for the time being), so it is conceivable that the observed animal only looked like a swan from a distance.

Further forms of scientific hypotheses and their verifiability can be found in Groeben and Westmeyer.

Computer science (verification of software)

The exam is one of the most important tasks in the development of complex, extensive software and safety-critical applications. Verification is used to determine whether a computer program corresponds to its specification (e.g. using the Hoare calculus ). The verification answers the question: "Is the product created correctly?" . With the help of verification, existing errors are tracked down.

Regardless of the technology used (methods, techniques and tools), however, verification cannot prove that the product under consideration is free of defects. The reason for this is that the requirements placed by the customer on the product are in non-formal form and therefore do not constitute a suitable input for the verification process. The task of verification in computer science is therefore to show that no errors have found their way into the development process after the specification was created. If the specification already contains errors, these are not (necessarily) proven by means of verification.

Manual / non-formal verification

Non-formal verification is essentially the dynamic and static testing to find errors that crept in during the development process. This type of verification is called non-formal because it is not based on mathematical proofs. The word manual shouldn't be taken too literally. Especially with large projects that are developed over a long period of time, it is common to have the tests carried out (partially) automatically with the help of programs. However, the evaluation of the results of test runs is often carried out manually.

Dynamic testing

This type of testing involves running the system under test. In everyday language, the term “testing” is always understood to mean this type of test. Dynamic testing involves running test cases that examine certain aspects of the system. Dynamic tests can be carried out in the natural environment of the system or in a simulation of the same.

Static testing

Static testing is the examination of a system or component without it being executed. In static testing, often referred to as analysis, the characteristics of a system or its components are assessed without its execution. (Design reviews, code inspection / walkthrough, checklists, formal evidence, control flow analysis and data flow analysis);

Automated / formal verification

Mathematical logic forms the basis for formal verification. As in a programming language, syntax and semantics are combined. While verification checks the output of a development phase for consistency with the previous phase, validation is used to compare the output of a development phase with customer requirements. The theorem proving and model checking are used as formal verification techniques to increase the quality of software.

Theorem proving

The theorem proving can be carried out on the basis of various logics. Peled describes the proving theorem using first-order predicate logic and the more restricted propositional logic . In order to be able to prove statements on the basis of a specification, a proof system is required that is suitable for the logic used. The proof system contains axioms and rules by means of which it can e.g. B. it is possible to prove that a formula is a tautology or that a formula is valid under a certain, given set of assumptions. An automatic theorem prover tries to transform and simplify the statement to be proven through skillful application of the rules so that its correctness can be determined.

Model checking

Model checking is another formal technique for verifying software. As theoretical computer science teaches, fully automatic verification is an insoluble problem for a broad class of programs. It cannot be expected that a verifier will be developed which receives a program and a specification as input and uses this data to decide fully automatically whether the program meets the specification. In order not to have to completely do without the support of a computer during the verification process in practice, the following measures can be taken:
  • Restriction to a smaller class of programs for which automatic verification algorithms exist. Model checking pursues this goal by restricting it to programs with a finite number of states.
  • Instead of verifying the entire system, one restricts oneself to a verification of the safety-critical parts, such as the algorithms or communication protocols on which the program is based.

Space travel

In space travel, which was shaped by NASA, a distinction is made between two activities under the generic term verification .

qualification

Formal proof that the draft meets all requirements of the customer requirements, including tolerances due to manufacturing, service life, defects, etc. and the parameters specified in the Interface Control Document ICD . The completion of the qualification is the signature of the client on the COQ (Certificate of Qualification). Qualification verification methods are:
  • Design review based on drawings (Review of Design / RoD). A code review is carried out for software.
  • analysis
  • Test (functions, mass, dimensions, etc.)
  • inspection

Each software element is tested individually and as part of the overall configuration, just like any other element of the system.

Decrease

Formal proof that the product to be delivered meets all requirements of the customer requirements (based on the serial number) and has no material or manufacturing defects. The acceptance is based on the proof of the successful, previous qualification (including the identity of the construction documents for the qualification model). The completion of the acceptance is the signature of the client on the COA (Certificate of Acceptance). Acceptance verification methods are:
  • test
  • inspection

The verification activities are the cause of the high cost of space equipment compared to the same technical product developed under normal industrial conditions. All the resulting results are documented and remain available for any later necessary error investigations. While these rules used to apply to all levels down to the component, attempts are now being made to reduce costs by using commercial components for non-safety-relevant devices.

While space travel was the pioneer for the development of miniaturized electronic components a few years ago, the extremely complex chips available are not readily usable for space travel. Their behavior under space radiation conditions (destruction or temporary misconduct) is mostly unknown or even cannot be tested on the ground. Hardware / software interaction analysis , which examines the reaction of hardware errors to the software running in the processor , has therefore become particularly important for stochastic errors. Large sums of money have been spent at NASA to date to find a commercial laptop that can be used on the ISS.

Another area that causes high costs is the qualification of the long-term behavior of materials in space because of the atomic oxygen. In many space programs, equipment and material lifetime qualification is greatly simplified in order to stay within budget; for example there are no cables that are certified for more than twelve years. The European Cooperation on Space Standards ( ECSS ) recently used the term verification to refer to the activities defined above under qualification ; the generic term verification is omitted.

quality control

The DIN EN ISO 8402 of August 1995, section 2.17 understands verification as "the confirmation on the basis of an investigation and by providing evidence that specified requirements have been met." This standard relates to the quality assurance of organizational and operational processes. Verification is understood here as a "retrospective confirmation" as to whether existing processes achieve the desired results.

ISO 8402 has been withdrawn, but all terms of quality management have been found in ISO 9000 since 2000. The last version ISO 9000: 2015, Section 3.8.12, defines verification as “confirmation by providing objective evidence (3.8.3) that specified requirements (3.6.4) have been met ". In contrast, ISO 9000: 2015, Section 3.8.13, describes validation as “Confirmation by providing objective evidence (3.8.3) that the requirements (3.6.4) have been met for a specific intended use or application ".

Example:

  • Confirmation that a product fulfills a company's own internal specification leads to a verified product.
  • Confirmation that a product fulfills a customer specification and thus the requirements for use by the customer leads to a validated product.

In a company, verification is usually carried out first and then validation. Above all, this is correct as long as EN ISO 9001: 2008 is followed and the customer requirements have been determined in the company and laid down in an internal specification sheet. The verification is a check of the conformity to the customer requirements formally laid down in the internal specifications. The validation, on the other hand, is a kind of field test to check whether the product really does what the customer wants in the application and is thus, among other things, a verification of the specification. A product that has been verified but not validated harbors a great risk that the user or customer will receive a product that may have very good properties and meet the internal specifications, but does not meet the customer's requirements in terms of application.

In computer science, this type of verification is compared to validation .

Authentication

The verification of personal data or protocols is known as the process of a joint signature or as a sovereign act of authentication . The related term authentication is also used here as a synonym for proof of identity . In colloquial language, verification is also used here in technical documentation.

Examples of verification

Military affairs

Verification is the name given to all those measures that serve to monitor compliance with disarmament or arms control agreements . The means of verification are technical systems (such as satellite monitoring), maneuver observers and inspectors.

Summary

The early verification or verification of a process or a statement helps to identify errors in good time and to avoid technical, human or procedural communication losses. Verification is not to be confused with validation .

The assessment of the content of the verified statements or data for plausibility or effect is not the task of verification. It is only a question of proving a certain authenticity of the statement itself. A verified expression (the result of an experiment) has thus been checked by a third party, but its scientific significance is not yet proven. The verified statement is therefore more important than the unsubstantiated claim , but less important than conclusive evidence . The proof no longer belongs to the realm of synthetic ( empirical ), but of analytical ( theoretical ) truth.

literature

  • Elliott Sober: Testability . In: Proceedings and Addresses of the American Philosophical Association 73, 1999, pp. 47-76 (PDF version; defense of the criterion).

Web links

Wiktionary: Verification  - explanations of meanings, word origins, synonyms, translations

Individual evidence

  1. ↑ N. Groeben and H. Westmeyer: Criteria for psychological research . Juventa, Munich 1975, pp. 107-133
  2. ↑ DIMAWEB-Interlexikon (technical terms): Die Verification dimaweb.at, December 4, 2015.
  3. ↑ Stewart Gardiner: Testing Safety-Related Software / Communication Networks, Springer-Verlag, London 1999, ISBN 978-1-4471-3277-6 .
  4. ^ A b Doron A. Peled: Software Reliability Methods / Software Engineering, Springer-Verlag 2001, ISBN 978-1-4757-3540-6 .
  5. ↑ University of Paderborn / Validation and verification (including testing, model checking and theorem proving) (PDF; 269.73 KB), January 24, 2016