Verifizierung

Verifizierung oder Verifikation (von lateinisch veritas ‚Wahrheit‘ und facere ‚machen‘) ist der Nachweis, dass ein vermuteter oder behaupteter Sachverhalt wahr ist. Der Begriff wird unterschiedlich gebraucht, je nachdem, ob man sich bei der Wahrheitsfindung nur auf einen geführten Beweis stützen mag oder aber auch die in der Praxis leichter realisierbare bestätigende Überprüfung und Beglaubigung des Sachverhaltes durch Argumente einer unabhängigen Instanz als Verifizierung betrachtet.

Metrologie

Im internationalen Wörterbuch der Metrologie^[1] wird die Verifizierung wie folgt definiert: Verifizierung ist die Erbringung eines objektiven Nachweises, dass eine Betrachtungseinheit die spezifizierten Anforderungen erfüllt. Dies ist beispielsweise der Nachweis, dass bei einem Messsystem die angegebene Messunsicherheit erreicht ist. Ergibt die Verifizierung, dass die spezifizierten Anforderungen auch für den beabsichtigten Zweck angemessen sind, ist das Ergebnis der Verifizierung eine Validierung des Messsystems für diesen Zweck.

Wissenschaftstheorie

In der Wissenschaftstheorie versteht man unter der Verifizierung einer Hypothese den Nachweis, dass diese Hypothese richtig ist. Logischer Empirismus und Positivismus gehen davon aus, dass solche Nachweise führbar seien. Im Rahmen des kritischen Rationalismus (Karl Popper) wird argumentiert, dass es Verifikation nicht gibt. Allgemeine Gesetzesaussagen können nur wahr, aber unverifiziert sein oder mit Beschreibungen von Sachverhalten, die der Aussage widersprechen, falsifiziert werden, sich also als ungültig herausstellen. Zum Verständnis ein Beispiel, das Karl Popper anführt: Angenommen, die Hypothese lautet: „Alle Schwäne sind weiß“, so trägt das Finden zahlreicher weißer Schwäne nur dazu bei, dass die Hypothese beibehalten werden darf. Es bleibt stets die Möglichkeit bestehen, einen andersfarbigen Schwan zu finden. Tritt dieser Fall ein, so ist die Hypothese widerlegt. Solange aber kein andersfarbiger Schwan gefunden wurde, kann die Hypothese weiterhin als nicht widerlegt betrachtet werden – also als „validiert“.

Auch bei lokalisierenden Existenzhypothesen (auch bestimmte Existenzhypothesen genannt) gilt der Falsifikationismus: Die (allgemeine) Hypothese „Es gibt weiße Schwäne“ kann für sich genommen nicht überprüft werden. Hat man jedoch den Aufenthaltsort eines weißen Schwans in einem Raum-Zeit-Gebiet, so ist die Falsifikation möglich, und zwar umso leichter, je eingeschränkter dieses Gebiet ist. Findet sich dort nämlich kein weißer Schwan, so kann die Hypothese als widerlegt betrachtet werden. Umgekehrt folgt die unfalsifizierbare Aussage „Es gibt weiße Schwäne“ aus einer solchen bestimmten Existenzhypothese wie „Am 25. August ist ein weißer Schwan im Augsburger Zoo“. Sie wird aber nicht bereits dadurch verifiziert, dass die Falsifikation (einstweilen) ausbleibt, so ist es denkbar, dass das beobachtete Tier nur aus der Ferne aussah wie ein Schwan.

Weitere Formen von wissenschaftlichen Hypothesen sowie deren Prüfbarkeit finden sich bei Groeben und Westmeyer.^[2]

Informatik (Verifizieren von Software)

Die Prüfung ist eine der wichtigsten Aufgaben bei der Entwicklung komplexer, umfangreicher Software und sicherheitskritischer Anwendungen. Mittels Verifikation wird festgestellt, ob ein Computerprogramm seiner Spezifikation entspricht (z. B. mit dem Hoare-Kalkül). Die Verifikation beantwortet die Frage: „Wird das Produkt richtig erstellt?“. Mit Hilfe der Verifikation werden vorhandene Fehler aufgespürt.

Unabhängig von der jeweils eingesetzten Technik (Methoden, Techniken und Werkzeuge) kann mittels Verifikation jedoch nicht nachgewiesen werden, dass das betrachtete Produkt fehlerfrei ist. Der Grund dafür liegt darin, dass die vom Kunden an das Produkt gestellten Anforderungen in nicht-formaler Form vorliegen und damit keinen geeigneten Input für den Verifikationsprozess bilden. Aufgabe der Verifikation in der Informatik ist es somit, zu zeigen, dass nach dem Zeitpunkt der Spezifikations-Erstellung keine Fehler in den Entwicklungsprozess Einzug gehalten haben.

Manuelle/nicht-formale Verifikation

Unter nicht-formaler Verifikation versteht man im Wesentlichen das dynamische und statische Testen, um Fehler, die sich während des Entwicklungsprozesses eingeschlichen haben, zu finden. Nicht-formal heißt diese Art der Verifikation, da sie nicht auf mathematischen Beweisen beruht. Nicht zu wörtlich sollte man das Wort manuell nehmen. Gerade bei großen Projekten, die über eine lange Zeit entwickelt werden, ist es üblich, die Tests mit Hilfe von Programmen (teil-)automatisch durchführen zu lassen. Oft wird jedoch die Auswertung der Ergebnisse von Testläufen manuell durchgeführt.^[3]

Dynamisches Testen

Diese Art des Testens beinhaltet die Ausführung des zu testenden Systems. In der Umgangssprache wird unter dem Begriff „Testen“ immer diese Art von Test verstanden. Beim dynamischen Testen werden Testfälle ausgeführt, die bestimmte Aspekte des Systems untersuchen. Dynamische Tests können im natürlichen Umfeld des Systems durchgeführt werden oder in einer Simulation desselben.

Statisches Testen

Statisches Testen ist die Untersuchung eines Systems oder einer Komponente ohne dessen/deren Ausführung. Beim statischen Testen, oft auch als Analyse bezeichnet, werden die Merkmale eines Systems bzw. seiner Komponenten ohne seine/ihre Ausführung begutachtet. (Design Reviews, Code Inspection/Walkthrough, Checklisten, formale Beweise, Kontrollflussanalyse und Datenflussanalyse);

Automatisierte/formale Verifikation

Mathematische Logik bildet die Basis für die formale Verifikation. Wie in einer Programmiersprache werden hierbei Syntax und Semantik kombiniert. Während die Verifikation jeweils den Output einer Entwicklungsphase auf Konsistenz mit der vorherigen Phase überprüft, wird die Validierung eingesetzt, um den Output einer Entwicklungsphase mit den Kundenanforderungen zu vergleichen. Als formale Verifikationstechniken werden das Theorem Proving und Model Checking eingesetzt, um die Qualität von Software zu erhöhen.

Theorem Proving

Das Theorem Proving lässt sich auf Basis verschiedener Logiken durchführen. Peled^[4] beschreibt das Theorem Proving anhand der Prädikatenlogik erster Ordnung und der eingeschränkteren Aussagenlogik. Um Aussagen auf Basis einer Spezifikation beweisen zu können, bedarf es eines Beweissystems, das passend zur verwendeten Logik ist. Das Beweissystem enthält Axiome und Regeln, mittels derer es z. B. möglich ist zu beweisen, dass eine Formel eine Tautologie ist oder dass eine Formel unter einer bestimmten, gegebenen Menge von Annahmen Gültigkeit besitzt. Ein automatischer Theorem Prover versucht durch geschickte Anwendung der Regeln die zu beweisende Aussage so umzuformen und zu vereinfachen, dass ihre Richtigkeit festgestellt werden kann.^[4]

Model Checking

Das Model Checking ist eine weitere formale Technik zur Verifikation von Software. Wie die theoretische Informatik lehrt, ist die vollautomatische Verifizierung für eine breite Klasse von Programmen ein unlösbares Problem. Es kann nicht erwartet werden, dass ein Verifizierer entwickelt wird, der als Eingabe ein Programm und eine Spezifikation erhält und anhand dieser Daten vollautomatisch entscheidet, ob das Programm die Spezifikation erfüllt. Um in der Praxis nicht völlig auf die Unterstützung eines Computers beim Verifikationsprozess verzichten zu müssen, können folgende Maßnahmen getroffen werden:

Beschränkung auf eine kleinere Klasse von Programmen, für die automatische Verifikationsalgorithmen existieren. Das Model Checking verfolgt durch eine Beschränkung auf Programme mit endlich vielen Zuständen dieses Ziel.
Statt das Gesamtsystem zu verifizieren, beschränkt man sich auf eine Verifizierung der sicherheitskritischen Teile, wie die dem Programm zugrundeliegenden Algorithmen oder Kommunikationsprotokolle.^[5]

Raumfahrt

In der von der NASA geprägten Raumfahrt unterscheidet man unter dem Oberbegriff Verifikation zwei Tätigkeiten.

Qualifikation

formeller Nachweis, dass der Entwurf alle Anforderungen des Lastenheftes (Customer Requirements) einschl. Toleranzen durch Fertigung, Lebensdauer, Fehler usw. und die im Schnittstellen-Kontroll-Dokument (Interface Control Document ICD) festgelegten Parameter erfüllt. Der Abschluss der Qualifikation ist die Unterschrift des Auftraggebers unter das COQ (Certificate of Qualification). Qualifikations-Verifikationsmethoden sind:

Entwurfsüberprüfung anhand von Zeichnungen (Review of Design / RoD). Für Software wird ein Code-Review durchgeführt.
Analyse
Test (Funktionen, Masse, Abmessungen usw.)
Inspektion

Jedes Software-Element wird einzeln und als Teil der Gesamtkonfiguration durch Test qualifiziert wie jedes andere Element des Systems.

Abnahme

formeller Nachweis, dass das abzuliefernde Produkt alle Anforderungen des Lastenheftes (Customer Requirements) erfüllt (bezogen auf die Seriennummer) und keine Material- oder Fertigungsfehler hat. Die Abnahme basiert auf dem Nachweis der erfolgreichen, vorhergehenden Qualifikation (einschließlich. Identität der Bauunterlagen zum Qualifikationsmodell). Abschluss der Abnahme ist die Unterschrift des Auftraggebers unter das COA (Certificate of Acceptance). Abnahme-Verifikationsmethoden sind:

Test
Inspektion

Die Verifikationstätigkeiten sind die Ursache für die hohen Kosten für Raumfahrtgeräte, verglichen mit einem gleichen technischen Produkt, das unter normalen Industriebedingungen entwickelt wurde. Alle dabei anfallenden Ergebnisse werden dokumentiert und bleiben verfügbar für eventuell später notwendige Fehleruntersuchungen. Während früher diese Regeln für alle Ebenen bis zum Bauelement galten, versucht man heute die Kosten durch Einsatz kommerzieller Bauelemente für nicht sicherheitsrelevante Geräte zu reduzieren.

Während vor einigen Jahren die Raumfahrt der Vorreiter für die Entwicklung miniaturisierter elektronischer Bauelemente war, sind die verfügbaren, extrem komplexen Chips nicht ohne weiteres für die Raumfahrt einsetzbar. Ihr Verhalten unter Weltraumstrahlungsbedingungen (Zerstörung oder zeitweiliges Fehlverhalten) ist meistens nicht bekannt oder kann sogar am Boden nicht getestet werden. Daher hat die Hardware / Software Interaction Analysis, die die Reaktion von Hardware-Fehlern auf die im Prozessor laufende Software untersucht, speziell für stochastische Fehler große Bedeutung erlangt. Bei der NASA wurden bis heute große Summen aufgewendet, um einen kommerziellen Laptop zu finden, der auf der ISS einsetzbar ist.

Ein weiteres, hohe Kosten verursachendes Gebiet ist die Qualifikation des Langzeitverhaltens von Materialien im Weltraum wegen des atomar vorkommenden Sauerstoffs. In vielen Raumfahrtprogrammen wird die Qualifikation der Lebensdauer von Geräten und Materialien stark vereinfacht, um im Kostenrahmen zu bleiben; zum Beispiel gibt es keine Kabel, die für mehr als zwölf Jahre zertifiziert sind. Neuerdings werden von der European Cooperation on Space Standards (ECSS) leider die oben unter Qualifikation definierten Tätigkeiten mit dem Begriff Verifikation bezeichnet; der Oberbegriff Verifikation entfällt damit und die klare Strukturierung der Prozesse geht damit verloren.

Qualitätssicherung

Die DIN EN ISO 8402 vom August 1995, Ziffer 2.17 versteht unter Verifizierung „das Bestätigen aufgrund einer Untersuchung und durch Bereitstellung eines Nachweises, daß festgelegte Forderungen erfüllt worden sind.“ Diese Norm bezieht sich auf die Qualitätssicherung von organisatorischen und betrieblichen Abläufen. Verifizierung wird hier also verstanden als eine „Bestätigung im Nachhinein“, ob vorhandene Abläufe die gewünschten Ergebnisse erzielen.

Die ISO 8402 ist zurückgezogen, aber alle Begriffe des Qualitätsmanagements findet man seit 2000 in der ISO 9000. Die letzte Version ISO 9000:2015, Abschnitt 3.8.12, definiert Verifizierung als „Bestätigung durch Bereitstellung eines objektiven Nachweises (3.8.3), dass festgelegte Anforderungen (3.6.4) erfüllt worden sind“. Im Gegensatz dazu beschreibt ISO 9000:2015, Abschnitt 3.8.13, Validierung als „Bestätigung durch Bereitstellung eines objektiven Nachweises (3.8.3), dass die Anforderungen (3.6.4) für einen spezifischen beabsichtigten Gebrauch oder eine spezifische beabsichtigte Anwendung erfüllt worden sind“.

Beispiel:

Bestätigung, dass ein Produkt ein unternehmenseigenes, internes Pflichtenheft erfüllt, führt zu einem verifizierten Produkt.
Bestätigung, dass ein Produkt ein vom Kunden erstelltes Lastenheft und damit so weit die Anforderungen an den Gebrauch durch den Kunden erfüllt, führt zu einem validierten Produkt.

Im Normalfall erfolgt in einem Unternehmen immer zuerst die Verifizierung und dann die Validierung. Dies ist vor allem deshalb richtig, sofern man die EN ISO 9001:2008 befolgt und im Unternehmen die Kundenanforderungen ermittelt und in einem internen Lastenheft festgeschrieben hat. Die Verifizierung ist eine Überprüfung der Konformität zur formal im internen Lastenheft festgehaltenen Kundenanforderungen. Die Validierung ist hingegen eine Art Feldversuch, um zu überprüfen, ob das Produkt in der Anwendung wirklich das leistet, was der Kunde haben will, und ist somit unter anderem eine Verifizierung des Lastenhefts. Ein Produkt, das zwar verifiziert, aber nicht validiert wurde, birgt große Gefahr, dass der Anwender oder Kunde ein Produkt erhält, das zwar sehr gute Eigenschaften haben kann und dem internen Lastenheft gerecht wird, aber nicht den Anforderungen des Kunden in der Anwendung entspricht.

In der Informatik wird diese Art der Überprüfung der Validierung gegenübergestellt.

Authentifizierung

Die Verifizierung von Personendaten oder Protokollen ist als Vorgang einer gemeinsamen Unterschrift oder als hoheitlicher Akt der Beglaubigung bekannt. Hier findet auch der verwandte Begriff der Authentifizierung als Synonym für einen Identitätsnachweis Verwendung. Umgangssprachlich wird hier oft auch in technischen Dokumentationen von Verifizierung gesprochen.

Beispiele für Verifizierungen

Nachweis einer genormten Vorgehensweise in einer Projektorganisation
Betrieblicher Abgleich von EDV-Protokollen
Empirischer Beleg der Wirksamkeit eines Medikamentes
Notarielle Beglaubigung einer Unterschrift
Überprüfung von Firmenadressen in einem Telefonverzeichnis
Der Abgleich von hinterlegten biometrischen Daten bei einer Zugangskontrolle
Nachweis von in Simulationen ermittelten Eigenschaften eines Produktes durch Experimente
Überprüfung von Online-Bestellungen durch Rückfrage beim Kunden
Nachweis, dass ein Benutzerkonto tatsächlich einer bestimmten Person gehört, siehe Kontoverifizierung

Militärwesen

Verifikation ist die Bezeichnung für alle diejenigen Maßnahmen, die der Überwachung der Einhaltung von Abrüstungs- beziehungsweise Rüstungskontrollabkommen dienen. Mittel der Verifikation sind technische Systeme (wie die Satellitenüberwachung), Manöverbeobachter und Inspektoren.

Zusammenfassung

Die frühzeitige Verifizierung beziehungsweise Verifikation eines Prozesses oder einer Aussage hilft, Fehler rechtzeitig zu erkennen und technische, menschliche oder prozessuale Kommunikationsverluste zu vermeiden. Verifizierung ist nicht zu verwechseln mit Validierung.

Die inhaltliche Beurteilung der überprüften Aussagen oder Daten auf Plausibilität oder Wirkung ist nicht Aufgabe der Verifizierung. Es handelt sich hierbei also nur um den Nachweis einer gewissen Authentizität der Aussage an sich. Ein verifizierter Ausdruck (das Ergebnis eines Experimentes) ist somit von Dritter Stelle überprüft, seine wissenschaftliche Aussagekraft ist damit jedoch noch nicht belegt. Die verifizierte Aussage hat somit zwar einen höheren Stellenwert als die unbelegte Behauptung, jedoch einen niedrigeren Stellenwert als der schlüssige Beweis. Der Beweis gehört allerdings nicht mehr zum Bereich der synthetischen (empirischen), sondern der analytischen (theoretischen) Wahrheit.

Literatur

Elliott Sober: Testability. In: Proceedings and Addresses of the American Philosophical Association 73, 1999, S. 47–76 (PDF-Fassung; Verteidigung des Kriteriums).

Weblinks

Wiktionary: Verifikation – Bedeutungserklärungen, Wortherkunft, Synonyme, Übersetzungen

Verifizierung von Lexikoneinträgen
VeriFun, ein semiautomatischer Beweiser für funktionale Programme

Einzelnachweise

↑ Burkhart Brinkmann: Internationales Wörterbuch der Metrologie. Grundlegende und allgemeine Begriffe und zugeordnete Benennungen (VIM) - Deutsch-englische Fassung ISO/IEC-Leitfaden 99:2007, korrigierte Fassung 2012. Hrsg.: DIN Deutsches Institut für Normung e. V. 4. Auflage. Beuth Verlag, Berlin 2012, ISBN 978-3-410-22472-3 (bipm.org – englisch: International Vocabulary of metrology (VIM). 2012.).
↑ N. Groeben und H. Westmeyer: Kriterien psychologischer Forschung. Juventa, München 1975, S. 107–133
↑ Stewart Gardiner: Testing Safety-Related Software / Communication Networks, Springer-Verlag, London 1999, ISBN 978-1-4471-3277-6.
↑ ^a ^b Doron A. Peled: Software Reliability Methods / Software Engineering, Springer-Verlag 2001, ISBN 978-1-4757-3540-6.
↑ Universität Paderborn /Validierung und Verifikation (inkl. Testen, Model-Checking und Theorem Proving) (PDF; 269,73 KB), 24. Jänner 2016

[1] Burkhart Brinkmann: Internationales Wörterbuch der Metrologie. Grundlegende und allgemeine Begriffe und zugeordnete Benennungen (VIM) - Deutsch-englische Fassung ISO/IEC-Leitfaden 99:2007, korrigierte Fassung 2012. Hrsg.: DIN Deutsches Institut für Normung e. V. 4. Auflage. Beuth Verlag, Berlin 2012, ISBN 978-3-410-22472-3 (bipm.org – englisch: International Vocabulary of metrology (VIM). 2012.).

[2] N. Groeben und H. Westmeyer: Kriterien psychologischer Forschung. Juventa, München 1975, S. 107–133

[3] Stewart Gardiner: Testing Safety-Related Software / Communication Networks, Springer-Verlag, London 1999, ISBN 978-1-4471-3277-6.

[Peled-4] Doron A. Peled: Software Reliability Methods / Software Engineering, Springer-Verlag 2001, ISBN 978-1-4757-3540-6.

[5] Universität Paderborn /Validierung und Verifikation (inkl. Testen, Model-Checking und Theorem Proving) (PDF; 269,73 KB), 24. Jänner 2016

[1]

[2]

[3]

[4]

[5]