Verifizierung
aus Wikipedia, der freien Enzyklopädie
Als Verifizierung oder Verifikation (von lat. veritas, Wahrheit) wird der Vorgang bezeichnet, einen vermuteten oder behaupteten Sachverhalt als wahr nachzuweisen. Der Begriff "Verifizierung" wird unterschiedlich gebraucht, je nachdem, ob man sich bei der Wahrheitsfindung nur auf einen geführten Beweis stützen mag, oder auch die bestätigende Überprüfung und Beglaubigung des Sachverhaltes durch eine unabhängige Instanz als Verifizierung betrachtet.
Inhaltsverzeichnis |
[Bearbeiten] 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. Heute wird jedoch allgemein im Rahmen des kritischen Rationalismus (K. Popper) davon ausgegangen, dass bestimmte Formen von Hypothesen (z. B. unbeschränkt universelle Hypothesen) nie letztgültig verifiziert, sondern theoretisch immer durch neueres Wissen überholt werden können. Eine Hypothese kann somit zwar falsifiziert werden, sich also als ungültig erweisen, jedoch kann nie mit Sicherheit angegeben werden, dass sie gültig sei.
Zum Verständnis ein Beispiel, das Karl Popper anführt: Angenommen, die Hypothese lautet: »Alle Schwäne sind weiß«, so hilft es nichts, sich auf die Suche nach möglichst vielen weißen Schwänen zu machen. Auch wenn wir eine Million weißer Schwäne gefunden haben, ist die Hypothese damit nicht verifiziert. Findet man jedoch auch nur einen andersfarbigen Schwan, so ist die Hypothese widerlegt. Allerdings: Solange kein andersfarbiger Schwan gefunden wurde, kann die Hypothese als vorläufig gültig betrachtet werden.
Der Falsifikationismus gilt allerdings nicht für alle Hypothesenarten. Bei lokalisierenden Existenzhypothesen (auch "bestimmte Existenzhypothesen") beispielsweise kehrt sich der Sachverhalt um: Zur Prüfung der Hypothese »Es gibt gegenwärtig in Deutschland weiße Schwäne« reicht es, einen weißen Schwan in Deutschland zu finden. Bei Hypothesen dieser Art ist eine Verifikation möglich. Findet sich kein weißer Schwan, so kann die Hypothese als vorläufig widerlegt betrachtet werden.
Weitere Formen von wissenschaftlichen Hypothesen sowie deren Prüfbarkeit finden sich in "Groeben, N. & Westmeyer, H. (1975). Kriterien psychologischer Forschung. Juventa: München." auf den Seiten 107-133.
[Bearbeiten] Informatik
In der Informatik und Softwaretechnik versteht man unter formaler Verifikation den mathematischen Beweis, dass ein Programm (also eine konkrete Implementation) der vorgegebenen Spezifikation entspricht (siehe Korrektheit (Informatik)). Solche Beweise werden mit Hilfe der Methoden der formalen Semantik geführt. Die Verifikation ist jedoch grundsätzlich nicht in jedem Fall möglich, wie das Halteproblem und der Gödelsche Unvollständigkeitssatz zeigen.
Da Beweise zur Verifikation zumeist außerordentlich groß und oft für den Menschen nicht intuitiv sind, werden interaktive oder automatisierte Theorembeweiser eingesetzt. Erstere basieren auf symbolischer Deduktion, während letztere spezielle Datenstrukturen verwenden. Während erstere zur Lösung sehr allgemeiner Probleme verwendet werden können, sind letztere nur in speziellen Bereichen (dann aber mit geringem Aufwand und geringen Vorkenntnissen) anwendbar.
Zur automatisierten Verifikation werden z.B. häufig Automatenmodelle eingesetzt. Für kleine Systeme mit endlicher Zustandsmenge (zum Beispiel im Hardwaredesign) werden dafür gerne Endliche Automaten eingesetzt (Model Checking), für parallele Prozesse finden Petri-Netze Verwendung. Aber auch andere Automaten können eingesetzt werden. Hintergrund ist die Möglichkeit, formale Spezifikationen in äquivalente Automaten zu überführen (z.B. zeigt der Satz von Büchi-Elgot-Trakhtenbrot die Äquivalenz von endlichen Automaten und Formeln der monadischen Logik 2. Stufe, siehe MSO), wobei das Problem des Erfüllens einer Spezifikation auf ein äquivalentes Problem der Analyse einer Eigenschaft des Automaten überführt wird. Automaten sind die geeignetere Repräsentation der Problemstellung zum Zwecke der Analyse, da hier gute Algorithmen bekannt sind.
Vergleiche: Validierung und Korrektheit.
Alternative Methoden zur Softwarequalitätssicherung: statische Analyse
[Bearbeiten] Raumfahrt
In der von der NASA geprägten Raumfahrt unterscheidet man unter dem Oberbegriff Verifikation die Tätigkeiten
- Qualifikation: formeller Nachweis, dass der Entwurf alle Anforderungen des Lastenheftes (specification) einschl. Toleranzen durch Fertigung, Lebensdauer, Fehler usw und die im Schnittstellen-Kontroll-Dokument (Interface Control Documend ICD) festgelegten Parameter erfüllt. Der Abschluss der Qualifikation ist die Unterschrift des Auftraggebers unter das COQ (Certificate of Qualification).
- Abnahme: formeller Nachweis, dass das abzuliefernde Produkt alle Anforderungen des Lastenheftes (specification) erfüllt (bezogen auf die Seriennummer). Die Abnahme basiert auf dem Nachweis der erfolgreichen, vorhergehenden Qualifikation (einschl. Identität der Bauunterlagen zum Qualifikationsmodell). Abschluss der Abnahme ist die Unterschrift des Auftraggebers unter das COA (Certificate of Acceptance).
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.
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 Bauelemte für nicht Sicherheits-relevante 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 zeitweises Fehlverhalten) ist meistens nicht bekannt bzw. kann sogar am Boden nicht getestet werden. Daher hat die "Hardware / Software Interaction Analysis", die die Reaktion von Hardware - Fehlern auf die im Processor laufende Software untersucht, speziell für stochastische Fehler grosse Bedeutung erlangt. Bei der NASA wurden bis heute grosse 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 12 Jahre zertifiziert sind.
Neuerdings werden von der "European Cooperation on Space Standards" (ECSS) die oben unter "Qualifikation" definierten Tätigkeiten mit dem Begriff "Verifikation" bezeichnet; der Oberbegriff "Verfikation" entfällt damit.
[Bearbeiten] 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.
In der Informatik wird diese Art der Überprüfung der Validierung gegenübergestellt.
[Bearbeiten] 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.
[Bearbeiten] Beispiele für Verifizierung
- 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
[Bearbeiten] Zusammenfassung
Die frühzeitige Verifizierung beziehungsweise Validierung eines Prozesses oder einer Aussage hilft, Fehler rechtzeitig zu erkennen und technische, menschliche oder prozessuale Kommunikationsverluste zu vermeiden.
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 (z. B. 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 ("emprischen"), sondern der analytischen ("theoretischen") Wahrheit.
Siehe auch: Validität, Reliabilität, Verifikationismus
