Diskussion:Verifizierung

Erste Anmerkung: Den Artikel bitte neu schreiben

Der Artikel sollte m.E. die verschiedenen Vorstellungen, die mit dem Begriff Verifizierung verknüpft sind, besser auseinanderhalten. Der verwandte Begriff Authentisierung muss besser eingeführt werden. Er ist nicht einfach ein Synonym. Evtl. ist eine Begriffsklärungsseite vorzuschalten. Der Artikel stellt ein Mélange her zwischen Wissenschaftstheorie, Rechtssprache, NLP-Ideen, Qualitätssicherungswesen und Alltagssprache. Er klärt nicht und macht als ganzes einen eher unbeholfenen Eindruck.
Was will der Autor sagen?
Ein Enzyklopädie-Artikel muss die Frage nach dem was, wo, wie und warum beantworten - und nicht im Sinne einer Assoziationskette irgendwie um den Begriff kreisen.
Der Artikel ist als Themavorgabe i.O. ich schlage aber vor, dass ihn jemand neu schreibt, der sich auskennt und Interesse daran hat. --HHK 00:37, 29. Jul 2003 (CEST)

Du kannst mich ruhig persönlich ansprechen, den Autor. Ich gebe gerne zu, dass ich kein Wissenschaftler bin. Aber dafür, dass hier so viele Wissenschaftler unterwegs sind, wundere ich mich, dass sich da überhaupt noch niemand mit befasst hat. Von daher danke für die Blumen. Zur Kritk habe ich eine Frage: wo genau findest Du in dem Artikel NLP-Ideen? Die haben da nämlich nichts drin zu suchen. Das würde mich mal ganz genau interessieren! Abgesehen davon ist die von dir monierte interdisziplinäre Ausrichtung einer Erklärung wohl ihre größte Stärke in einer allgemeinen Enzyklopädie. Danke für die Kritik! Bo 00:44, 29. Jul 2003 (CEST)

Begriffsklärung

Als Verifizierung wird die Beglaubigung oder bestätigende Vergleichsmessung zu einer Aussage bezeichnet.
Eine verifizierte Aussage ist wahr, ihre wissenschaftliche Allgemeingültigkeit ist damit jedoch noch nicht belegt. Die dazu notwendige Untersuchung nennt sich im wissenschaftlichen Rahmen Falsifizierung.
Meinst Du das im Ernst? Eine beglaubtigte (juristischer Akt) Aussage ist wahr? Aufgrund einer bestätigenden Vergleichmessung ist eine Aussage wahr? Und wenn sie wahr wäre, und das durch die Verifizierung nach Deiner Auffassung offensichtlich klar gemacht wird, warum sollte sie dann nicht wissenschaftlich allgemeingültig sein? Und wie werden Aussagen durch "Falsifizierung" (besser Versuche der Falsifizierung) allgemeingültig? Ich unterstütze HHKs Vorschlag entschieden!
(Der vorstehende Beitrag stammt von 129.187.254.11 – 04:39, 29. Jul. 2003 (MESZ) – und wurde nachträglich unterschrieben.)

Hilfe! Ich habe mich auf ein Gebiet gewagt, von dem ich nicht sehr viel verstehe! Ich bekenne mich schuldig! ;-)) Aber so stand es in den diversen Lexika die ich zu fassen bekommen habe. Und jede Menge Internetseiten, die diese Begriffe (offensichtlich falsch) verwendet haben. Bitte schnell korrigieren. Ich bin nämlich echt neugierig, was ich bei meiner nicht vorhandenen wissenschaftlichen Ausbildung versäumt habe. *ggg* Danke! Bitte besser machen, ich kann es kaum erwarten *liebguck* Bo

Mut zur Bearbeitung

Hey Leute! Generell gilt: Sei mutig beim ändern der Seiten! - also nicht nur rummeckern, wenn ein Artikel nicht gefällt, sondern "Bearbeiten"-Link klicken und direkt verbessen! Uli 09:09, 30. Jul 2003 (CEST)

...*ggg*... ich glaube nämlich, das war gar nicht sooo einfach, diesen Begriff vernünftig zu erklären. Da gab es so viele verschiedene Sinnzusammenhänge, dass wahrscheinlich nicht nur ich erst mal verzweifelt bin. Wahrscheinlich hatte auch deswegen bisher nie jemand Bock , das zu machen. Aber ich denke die Einteilung, die nun da steht, ist gar nicht so übel. Aber die Falsifizierung, die sollte in jedem Fall drin bleiben, sie ist doch sowas wie das Zwillingselement der Verifizierung in der Beweisführung, oder ?Bo

(Der vorstehende Beitrag stammt von Wiska Bodo – 09:25, 30. Jul. 2003 (MESZ) – und wurde nachträglich vollständig – mit Zeitangabe – unterschrieben.)

Nein, ist sie leider nicht. Wenn eine Theorie falsifiziert ist, ist zwar etwas bewiesen, nämlich dass sie nicht stimmt. Aber mit einer Falsifizierung kann man keine Theorie beweisen - das kann man nämlich nie. Uli 09:01, 31. Jul 2003 (CEST)

Wissenschaftstheorie?

Als Verifizierung (lat. veritas, Wahrheit) wird die bestätigende Überprüfung und Beglaubigung eines vermuteten oder behaupteten Sachverhaltes durch eine unabhängige Instanz bezeichnet. Der Begriff "Verifizierung" wird in unterschiedlichen Bereich leicht unterschiedlich gebraucht.
Wissenschaftstheorie
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. Eine verifizierter Ausruck (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.
Ich würde mal gerne wissen, von welchem Wissenschaftstheoretiker oder welcher wissenschaftstheoretischen "Schule" der Begriff "Verifizierung" so verwendet wird. Das ist jedenfalls nicht die Weise, wie der Begriff normalerweise in der Wissenschaftstheorie verwendet wird. (Abgesehen davon, daß Teile dieses Zitats IMHO völlig unverständlich sind. Was soll das etwa heißen: Es handelt sich hierbei also nur um den Nachweis einer gewissen Authentizität der Aussage an sich. Sehr präzise und deutlich ist das in jedem Fall nicht.) Mein Verdacht: Das wird von keinem Wissenschaftstheoretiker so gesagt, deshalb nehm ich das mal raus.
(Der vorstehende Beitrag stammt von 129.187.254.11 – 01:42, 31. Jul. 2003 (MESZ) – und wurde nachträglich unterschrieben.)

Ich nehm das mal wieder rein. Bitte nicht einfach Passagen rauswerfen, wenn weil man es angeblich besser weiß. Du weißt es anscheinend besser ("Das ist jedenfalls nicht die Weise, wie der Begriff normalerweise in der Wissenschaftstheorie verwendet wird.") - also wär's nett, wenn Du das entsprechend im Artikel einpflegen könntest. Alles andere ist schlechter Wikipedia-Stil Uli 09:01, 31. Jul 2003 (CEST)

Ich verstehe nicht, warum Fehlinformationen guter Wikipedia-Stil sein sollen. (Außer man möchte, daß Wikipedia von Fachleuten nicht ernst genommen wird.) Zumal der Artikel auch ohne den falschen Abschnitt Bestand hätte. (Deswegen haben ich gewagt, ihn rauszunehmen.) Jetzt haben wir halt einen Artikel mehr, der dem Ansehen der Wikipedia schaden kann. Schade, aber man kann da offensichtlich nichts machen.

Allgemein gesagt: Ich bin entschieden der Meinung: Besser nix als Falsches.

(Der vorstehende Beitrag stammt von 129.187.254.11 – 18:31, 31. Jul. 2003 (MESZ) – und wurde nachträglich unterschrieben.)

Ich bin entschieden der Meinung: Besser was Richtiges, als was Falsches. Mit nur Löschen und nur in der Diskussion vermerken, dass es ja "alles falsch sei" und man es viel besser wüsste, aber sein Wissen lieber für sich behält, ist niemandem geholfen. Uli 19:07, 31. Jul 2003 (CEST)

Die Wahl habe wir aber im Moment nicht, da im Moment niemand bereit und fähig ist, die Diskussion zum Thema "Verifizierung" aus wissenschaftstheoretischer Sicht korrekt darzustellen. Die Wahl ist nix oder was Falsches.

Mit Löschen wäre der Wikipädia geholfen, da weniger Falsches drin stünde. Und den unbedarften Lesern, da die Wikipädia ihnen keinen Bären aufbinden würde.

(Der vorstehende Beitrag stammt von 129.187.254.14 – 21:20, 31. Jul. 2003 (MESZ) – und wurde nachträglich unterschrieben.)

Pardon, aber Wikipedia wird von Fachleuten eh nicht "ernst" genommen. Es kann allenfalls als Anhaltspunkt für weitere Recherchen sein, z.B. durch weitere Begriffe und einem gewissen Kontext, in den das zu suchende gebracht wird. Ob das ganze dann _stimmt_ oder (wie leider so oft) nur Halbwahrheiten sind, ist bei einem offenen System noch weniger zu überschauen, wie bei "klassischen", gedruckten Lexika. - und diese gelten bei Fachleuten ebenfalls nicht als sichere Quelle.

(Der vorstehende Beitrag stammt von 84.163.73.79 – 22:25, 17. Apr. 2007 (MESZ) – und wurde nachträglich unterschrieben.)

Model Checking

Ich habe da ein paar Fragen zum Model Checking:

• Wird dieser Begriff wirklich nur für Modelle benutzt, die als endliche Automaten modelliert werden?
• Warum wird ein EA gewählt, obwohl sich sehr viele einfache Vorgänge gar nicht allgemein abbilden lassen (wie zum Beispiel dass Zählen...)?
• Ist Model Checking mit EAs weiter verbreitet als z.B. Verifikation mittels Petri-Netzen? Wenn nein, warum wird dieses hier nicht erwähnt?
• Wenn sich nur kleine Systeme mit EAs checken lassen (und das ist so), dann trifft es wohl zu, dass dieser Ansatz eigentlich nur für Hardware relevant ist. Das sollte evtl erwähnt werden...

Könnte da jemand Licht in die Sache bringen?
-- D. Düsentrieb (?!) 23:48, 30. Aug 2004 (CEST)

Lieber Daniel,

Du weisst vielleicht, dass endliche Automaten und reguläre Ausdrücke äquivalent sind, d.h. zu jedem endlichen Automaten kann ich einen regulären Ausdruck angeben, der die vom Automaten erkannte Wortmenge beschreibt und umgekehrt.

Nun gibt es eine weitere Äquivalenz: Man kann logische Formeln über Wortmodellen betrachten, wo bestimmte Worte die Formeln erfüllen und dazu einen äquivalenten Automaten angeben (und umgekehrt).

Mit den logischen Formeln kann man sehr schön Spezifikationen verfassen, die endlichen Automaten sind aber besser geeignet um darauf Algorithmen anzuwenden, die z.B. feststellen welche Eigenschaften der Automat bzw. die von ihm erkannte Sprache hat.

D.h. die Frage, ob eine bestimmte Belegung logischer Variablen eine logische Formel erfüllt, lässt sich auf eine äquivalente Frage zu einer Eigenschaft eines endlichen Automaten abbilden, für die man viele Algorithmen kennt.

Deine Frage ist insofern nicht korrekt, die Automaten treten letztlich nur als andere Form der logischen Spezifikationen auf.

Es sei noch gesagt, dass nicht nur das intuitive System der Logik gibt, die man so aus dem mathematischen Alltag kennt. Die Logiker untersuchen ganz bestimmte Logiksysteme und verpassen ihnen Namen, so wie es die Komplexitätstheoretiker mit ihren Problemen machen (z.B. TSP = Traveling Salesman,..). Z.B. FO (first order), MSO (monadic second order) oder LTL und CTL.

Bei der Betrachtung der Automaten wird man auf deterministische Automaten wandeln wollen, dazu verwendet man die Potenzmengenkonstruktion. Daher kann die Zahl der Zustande exponentiell anwachsen. Das ist dann aber auch schon wirklich der ungünstigste Fall. Ganz so pessimistisch muss man nicht sein. In der Praxis kann man sehr wohl eine grosse Klasse von Spezifikationen beherrschbar (ohne kombinatorische Explosion der Zustände) wandeln.

Die Situation ist nicht unähnlich dem Turing Halteproblem, klar man kann nicht beliebige Programme auf bestimmte Eigenschaften (wie Halten) durch ein Programm testen. Aber das gilt dann wirklich für alle noch so pathologischen Fälle. Muss man gleich die Flinte ins Korn werfen? Nein, Du siehst z.B. an Compiler Warnungen und Fehlern, das trotz Turings Aussage offenbar für viele Programme schon eine Prüfung praktibel ist. :)

Schau mal in die Vorlesung von Prof. Thomas.

--Marc van Woerkom 14:38, 31. Aug 2004 (CEST)

Hallo Marc. Ich stimme dir in allen Punkten zu, und erhalte dennoch alle meine Fragen aufrecht. Vielleicht reden wir aneinander vorbei? Ich versuch mal, meine Fragen zu präzisieren:

• Mir ist wohl bewusst, dass sich jede logische Formel als Automat modellieren lässt. Allerdings im Allgemeinen nicht als endlicher Automat: das geht nur mit aussagenlogischen Formeln, bei der Prädikatenlogik geht das nicht mehr. Aussagenlogische Spezifikationen sind aber schon in sehr einfachen Fällen nicht mehr ausreichend.
• Endliche automaten sind schon mit dem Zählen überfordert. So kann ich mir zum Beispiel keinen EA vorstellen, der eine Funktion verifiziert, die die Eingabe auf korrekte Klammerung überprüft (auch keinen nichtdeterministischen, DEAs und NEAs sind ja bekanntlich äquivalent in Bezug auf die Mächtigkeit).
• Die Schwierigkeit mit endlichen Automaten liegt in ihrer Endlichkeit: Sobald die Länge der Eingabe unbegrenzt ist und die Eingabe u.U. in ihrer Gänze betrachtet werden muss, reicht ein EA nicht mehr aus. Im Hardwareentwurf dürften EAs ein gutes Modell sein, das meist die Eingabe durch die Wortbreite begrenzt ist. Bei Algorithmen zum Sortieren etc. ist aber die Länge der Eingabe unbegrenzt.
• Petri-Netze verdienen wohl eine Erwähnung als Modell für parallele Prozesse. Das ist völlig unabhängig von den anderen Fragen. Eine Erweiterungen der klassischen Petri-Netze sind übrigens turing-mächtig und können daher als allgemeines Modell für die Verifikation eingesetzt werden.

Ich hoffe, das macht meine Fragen ein wenig deutlicher. -- D. Düsentrieb (?!) 15:05, 31. Aug 2004 (CEST)

ich versuch mal ein bisschen was:

• eigentlich handelt es sich nicht um EAs, sondern um eine "Weiterfuehrung" davon, die sog. Kripke-Strukturen. Die den Petri-Netzen vermutlich schon recht aehnlich sind -- so gut kenn ich mich mit der Sache denn doch nicht aus. Wer weiss mehr?

Vermutlich alles, was nicht erwaehnt ist, liegt an meinem mangelnden Wissen darueber -- Besserwisser gesucht! --Pinguin.tk 17:54, 31. Aug 2004 (CEST)

Dann sollte unbedingt die Aussage, dass die Verifikation über Endliche automaten läuft, da raus: das ist extrem irreführend. Auch die angabe über die Komplexität ist sehr schwammig: was, bitte, it ein System der Grösse O(n)? Grösse von was? Die Eingabe kann es ja wohl nicht sein. Und die Anzahl der zustände ist im Allgemeinen unendlich...

Ach ja: schreib och mal einen Artikel über die Kripke-Strukturen - darüber weis ich nämlich nichts. Und schau mal weiter unten, was da über Büchi Automaten steht - hat das damit was zu tun? -- D. Düsentrieb (?!) 18:03, 31. Aug 2004 (CEST)

Hab den Artikel Model Checking etwas geaendert, ist es so besser? Sowohl Buechi- als auch Muller-Automaten haben was mit Model Checking und Kripke-Strukturen zu tun, auch CTL und LTL sollten erwaehnt werden.. mir fehlt da grad leider die Zeit, aber ich glaube, Marc kennt sich damit ziemlich gut aus, vielleicht kann er ja was schreiben? Pinguin.tk 18:31, 31. Aug 2004 (CEST)

Ja, besser, danke! Allerdings sollte da auch stehe, dass das nur für Algorithmen mit endlichem (also O(k)) Speicherbedarf funktioniert. Also nicht für "kleine Systeme", sondern nur für Probleme mit geringer (konstanter!) Speicherkomplexität, bzw. bei extrem beschränkter Eingabelänge. In der Praxis kann das desshalb IMHO eigentlich nur im Hardwarebereich sinnvoll sein. -- D. Düsentrieb (?!) 18:39, 31. Aug 2004 (CEST)

Ein Model (ein EA, Algorithmus etc.) der keine beschränkten speicherbedarf hat ist nicht verifizierbar, aber auch nicht simulierbar. Von sowas träumen eh nur die Informatiker da es nur im abstrakten soetwas gibt wie "unendlichen Speicher". Allerdings lässt sich über die verifikation nachweisen das ein Model, sei es ein Software-Algorithmus doer Hardware, eine obere schranke des Speicehrverbrauchs nicht überschreitet. Da ich Verifikation im Allgemeinen und auch speziellen Vertiefe, nehm ich mir mal bei zeiten ein oder zwei Bücher in die Hand und erweitere den Artikel um "Formale Verifikation", eventuell nen Artikel zu Kripke-Strukturen bzw. Kripke-Model. Es muss nur jemand meine Rechtschreibfehler Korrekturlesen *g* -- Haihaeppchen 20:44, 26. Mär. 2011 (CET)

Endliche Automaten

Was das Automaten Modell angeht: wenn ich mich recht erinnere, waren das Büchi Automaten, also Automaten mit endlich vielen Zuständen, aber einer anderen Definition, wann ein eingelesenes Wort akzeptiert wird, so dass auch Wörter unendlicher Länge erkannt werden können. Z.B. wenn ein als Endzustand ausgezeichneter Zustand beim Lesen des unendlichen Wortes unendlich oft durchlaufen wird, wird das Wort aus $\Sigma ^{\omega }$ akzeptiert.
Das ist keine unübliche Bedingung. Turing Maschinen, werden vergleichbar zu Typ-2 Maschinen erweitert, damit reelle Zahlen erkannt werden können. (Wieder ein Link für die Wikipedia :-)
Ich acker das gerne nochmal bei Gelegenheit durch, der Äquivalenzssatz, auf den ich mich beziehe, war von Büchi-Elgi-Trachtenbrot (Rechtschreibung muss ich nochmal prüfen :-)
Das nur bestimmte (einfache) Logiken betrachtet werden, hatte ich schon erwähnt, also FO, MSO, LTL ..
Endliche Automaten haben endlich viele Zustände und damit letztlich nur ein endliches Gedächtnis, für die Erkennung von Klammerungen braucht man potentiell unendlich viel Speicher, daher ist das auf der Chomsky Hierarchie auch eine Ebene höher (Pushdown Automaten <-> Kontextfreie Grammatiken). Folglich dürfe man auch mit der zugelassenen Logik kein Zählen über |N modelieren können, wohl aber Zählen in endlichen Ringen, wie Zählen modulo 3.
Büchi Automaten können durchaus unendliche Worte analysieren, allerdings nur, solange endlich viel Speicher dafür ausreicht.
Mit den Petri Netzen zur Modelierung Paraleller Prozesser stimme ich Dir zu, auch Da findest Du einiges in den Vorlesungen von Prof. Thomas (siehe Links auf der Seite zu den finiten Automaten). Ob es dazu auch eine Wiki Seite gibt? Da müssten dann noch so Dinge wie das Pi Kalkül (die parallele Variante des Lambda Kalküls) rein.
Ansonsten schau doch mal in den SMV Model Checker, da siehst Du mal reales model checking. Link klemme ich gleich auf die Artikelseite.
--Marc van Woerkom 15:58, 31. Aug 2004 (CEST)

Das ist alles sehr richtig, was du sagst. Das Problem liegt, wie gesagt, im endlichen Speicher: deine Aussagen über den Büchli-Automaten treffen genau so für alle endlichen Automaten zu, Moore, Mely, etc - auch die können unbegrenzt lange wörter akzeptieren, solange sie nicht Zählen müssen, d.h. a*ba* kann erkannt werden, aⁿbaⁿ nicht. Wenn also auch nur ein Zähler benötigt wird, braucht man mindestens einen Kellerautomaten - das ist übrigens schon bei der FO-Logik (zu deutsch Prädikatenlogik 1. Ordnung) der Fall, wenn ich mich recht erinnere.

Der Punkt ist: die wenigsten Algorithmen kommen bei unbegrenzter Eingabe mit begrenztem Speicher aus, und diese sind ohnehin meist trivial. Alle anderen können mit endlichen Automaten nicht verifiziert werden, und desshalb ist diese Methode bei der Software-Verifikation kaum von Bedeutung. Bei der Verifikation von Schaltungen sieht das anders aus.

Es wäre übrigens super, wenn du was über die Büchli-Automaten schreiben könntest - von denen hatte ich noch nie gehört. Insbsondere würde mich der Äquivalenzsatz interessieren - besonders, zu welcher Logik der Äquivalent ist. Soweit ich weiss kann er, bei endlichem Speicher, nicht mächtiger sein als ganz normale endliche Automaten.

Zu Petri-Netzen sollte man wohl noch mehr schreiben, und auch einen Verweis in diesen Artikel einbauen. Wenn du was über das Pi-Kalkül beisteuren könntest, wäre das toll - darüber weiss ich nämlich nichts.

-- D. Düsentrieb (?!) 17:48, 31. Aug 2004 (CEST)

Automatentheorie

Automatentheorie wird ja normal nur ein bisschen im Informatikstudium angeschnitten, daher war ich begeistert, dass man via ULI die Vorlesungen eines Spezialisten dazu lesen/schauen konnte. Der brachte halt auch die Verweise zur Modellierung paralleler System, sowie Spieltheorie und Model-Checking. Auch interessant: die Automaten, die nicht auf Strings sondern auf Bäumen operieren. Hat sogar Anwendungen bei den XML Technologien und im Compilerbau. Die Links stehen ganz unten bei auf Finite Automaten.
Ich konnte damals nicht alles durchackern (zu wenig Zeit), nehme mir aber seit längerem vor, alles in Ruhe nochmal durchzugehen. Diesen Vorlesungszyklus in einen Haufen Wiki Artikel zu verwandeln wäre eine ideale Gelegenheit.
Das Pi Kalkül stammt von Robin Milner (Autor von SML) und ist ein Versuch parallele Prozesse formal in den Griff zu bekommen.
--Marc van Woerkom 18:08, 31. Aug 2004 (CEST)

Mehr Artikel zum Thema Automatentheorie wäre toll - aber trag doch erstmal alle Automatenmodelle, die du kennst, in den Artikel Automat (Informatik) ein. Du musst nicht gleich Artikel dazu schreiben: Rote Links sind gut! Die zeigen, was noch fehlt! Danke jedenfalls für deine anregenden Infos -- D. Düsentrieb (?!) 18:25, 31. Aug 2004 (CEST)

Mache ich. Freut mich, dass euch diese Themen auch interessieren. --Marc van Woerkom 21:29, 31. Aug 2004 (CEST)

Ungültig/Gültig? oder: Bestimmt oder Unter-/Überbestimmt

"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."
Es kann also nie mit Sicherheit angegeben werden, daß es gültig ist, daß sich eine Hypothese als ungültig erweist. Es kann also falsifiziert werden, daß es gültig ist, daß eine Hypothese falsifiziert werden kann. Es kann also falsifiziert werden, daß es gültig ist, daß es sich um eine Hypothese handelt. Kann sich nur das Objekt "Hypothese" oder auch das Objekt "Gegenstand" als falsifizierbar erweisen?
"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."
Das ist ja auch ein unterbestimmter Satz: es fehlt Mengenangabe: wieviele? nur einen? Leicht falsifizierbar. bestimmte Anzahl? Alle Schwäne? Zählen auch tote mit, auch Schwäne, denen das Federkleid fehlt, die aber an sich weiß sind? Zudem: Der Schwan ist Deutschland, er ist nicht Deutschland.
134.2.222.69 01:48, 28. Apr 2006 (CEST)

Falsifikation

Die Weblinks zu Coverity und Polyspace habe ich entfernt und nach statische Analyse verschoben. Beides sind Falsifizierer, sprich Werkzeuge zum Nachweis von Fehlern, aber nicht Werkzeuge zum Nachweis der Erfüllung von Anforderungen. --Jens611 08:18, 12. Mär. 2007 (CET)

Beweis

Gibt es als logischen oder mathematischen Beweis, wobei der mathematische Beweis ein logischer Beweis IST - laut mathematischer Grundlagen - aber in der WP nicht ganz korrekt dargestellt wird. Ich hoffe, das wird in nächster Zeit korrigiert - sonst müßte ich wohl einen QA stellen. Ein Ansatz ist ja schon da, indem Beweis auf eine BKL verlinkt war. --SonnInfo 14:50, 25. Sep. 2007 (CEST)

Hilfe:Unterschreiben

Also lest bitte mal Wikipedia:Signatur und kennzeichnet eure Beiträge. Eure Korrigierereien von Beiträgen diverser IPs ohne Signatur sind nachträglich nicht mehr sauber zurückzuverfolgen. --SonnInfo 15:17, 25. Sep. 2007 (CEST)

Überarbeiten 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)).
Erst mal sind Informatik und Softwaretechnik verwandt, aber verschiedene Paar Stiefel. Von daher wirft der Artikel schon am Anfang eine Nebelkerze. Man kann vielleicht einen Algorithmus mit mathematischen Mitteln verifizieren, aber keine konkrete Implementation. Also grober Unfug.
Der Rest des Artikels schien in Ordnung zu sein wenn man ihn als die Verifikation eines Algorithmus versteht, aber bestimmt nicht OMA-tauglich.--Avron 18:26, 9. Jul. 2008 (CEST)

Natürlich kann man das. Dazu gibt es seit den 70ern das Hoare-Kalkül. Ein in der Praxis einsetzbarer Formalismus ist OCL. 132.231.1.64 10:47, 2. Feb. 2009 (CET)

Bei der Verifikation von Software wird häufig auch ein "golden device" verwendet. Es hat die gleiche Funktion wie der Ur-Meter oder das Ur-Kilo in Paris. Jeder Wartungsarbeit, Erweiterung, Veränderung wird mit diesem golden device überprüft. Bereits festgelegte Funktionalitäten, (Mess-)Ergebnisse, Daten (z.B.Korrekturwertkurven) usw. müssen sich nach Änderungen an der software mit dem golden device wieder reproduzieren lassen. Verifikation von software kann sich also nicht nur auf eine Einhaltung von Endergebnissen bestimmter Algorithem beziehen, die sich innerhalb der software befinden, sondern auch auf Objekte die von der software bearbeitet/verändert oder bewertet werden. Wenn ein bei einer Robotersteuersoftware ein Sortieralgorithmus durch einen anderen Algorithmus ersetzt wird, dann kann man das Ergebniss mit einem genau festgelegten Objektsortiment verifiziert werden. Ist der neue Algorithmus gleich gut, schlechter oder besser oder versagt er total bei der als Referenz definierten Aufgabe? So kann man einen Vergleich über die Lebens/Einsatzzeit der software durchführen im Hinblick auf Funktionalität, Leistungsvergleich und Reproduzierbarkeit von Ergebnissen. Der Einsatz von golden device ist nicht unbedenklich, da die Ergebnisse wesentlich von dem Zustand des devices abhängen. Der Einsatz von Arbeitskopien oder der Ringvergleich mehrerer golden device ist ratsam. Verifikation von Software/Softwaretechnik bezieht sich also nicht nur auf mathematische Beweise sondern auch immer auf die Ergebnisse die diese software mit der "Aussenwelt" produziert. Oft ersetzt diese Ergebnissanalyse die eigentliche Verifikation, der den Ergebnissen zugrunde liegenden Algorithem, da sie sich oft mit weniger Aufwand an die Qualifikation der Verifizierers realisieren lassen und damit Kosten und Zeit sparen.
(Der vorstehende Beitrag stammt von 89.54.182.42 – 22:47, 22. Jul. 2008 (MESZ) – und wurde nachträglich unterschrieben.)

Das was du schreibst verstehe ich eher als Regressionstest, einem Vergleich mit dem früheren Verhalten. Eine Verifikation ist das nicht. --Avron 13:59, 25. Aug. 2008 (CEST)

Validierung / Verifizierung

• Validierung: Aufbau, Kapazität, Struktur, Statik; KANN es funktionieren bzw. das gewünschte Ergebnis bringen / produzieren; strukturell/konstruktionsbedingt, ist es richtig konstruiert und gebaut? STRUKTUR-Parameter / Attribute (statisch)
• Verifizierung: Ablauf, Verhalten, Methode, Funktion, Ergebnis, Dynamik: HAT es funktioniert bzw. das gewünschte / erwartete Ergebnis produziert / gebracht? Ist es richtig abgelaufen. Zeigt es das richtige Verhalten. VERHALTENS-Parameter / Messwerte (dynamisch) (nicht signierter Beitrag von 134.106.119.31 (Diskussion) 18:24, 15. Aug. 2015 (CEST))

Verifizieren bedeutet in der Informatik, geprüft wird, ob eine Implementierung korrekt im Sinne seiner Spezifikation ist. Dies wird in der Softwareentwicklung durch Tests nachgewiesen. (Haben wir es richtig gebaut?)

Validieren bedeutet in der Informatik, dass geprüft wird, ob die Implementierung tatsächlich das zu lösende Problem löst. Dies wird in der Regel durch Scenarien geprüft. (Haben wir das richtige gebaut?) (nicht signierter Beitrag von 192.54.144.229 (Diskussion) 12:09, 18. Jan. 2016 (CET))

Um mir das klar zu machen habe ich die Wikipedia Artikel Verifizierung und Validierung_(Informatik) aufgerufen. Dort steht das aber nicht. Wie wäre es diese beiden Punkte im Artikel gleich am Anfang zu bringen? --MagHoxpox (Diskussion) 10:42, 31. Jul. 2017 (CEST)

Verifikationismus

kommt im Lemma bisher nicht vor

mir fehlt gerade die Zeit mich tiefer einzuarbeiten um festzustellen wie und wo das einzufügen wäre

vielleicht kann das ja jemand anderes übernehmen

Gruß --Über-Blick (Diskussion) 23:07, 17. Sep. 2022 (CEST)