verifikation

Verifikation eller verifikation (fra latinsk veritas 'sandhed' og facere ' at gøre') er bevis for, at en mistænkt eller påstået kendsgerning er sand . Udtrykket bruges forskelligt afhængigt af, om sandhedens konstatering kun kan baseres på tilvejebragt bevis, eller om den lettere realiserbare bekræftende undersøgelse og certificering af fakta gennem argumenter fra en uafhængig myndighed betragtes som verifikation.

Metrologi

I den internationale metrologiordbog defineres verifikation som følger: Verifikation er tilvejebringelse af objektive beviser for, at en enhed, der overvejes, opfylder de specificerede krav. Dette er for eksempel et bevis på, at den specificerede måleusikkerhed er opnået i et målesystem. Hvis verifikationen viser, at de specificerede krav også er passende til det tilsigtede formål, er resultatet af verifikationen en validering af målesystemet til dette formål.

Videnskabsfilosofi

I videnskabsfilosofien er verifikation af en hypotese beviset for, at denne hypotese er korrekt. Logisk empiri og positivisme antager, at sådanne beviser er mulige. I forbindelse med kritisk rationalisme ( Karl Popper ) hævdes det, at verifikation ikke eksisterer. Generelle juridiske erklæringer kan kun være sande, men ubekræftede, eller de kan forfalskes med beskrivelser af fakta, der strider mod udsagnene, dvs. de kan findes at være ugyldige. For at forstå et eksempel givet af Karl Popper: Hvis vi antager, at hypotesen er: "Alle svaner er hvide", hjælper det kun med at finde talrige hvide svaner at sikre, at hypotesen kan opretholdes. Der er altid mulighed for at finde en anden farvet svane. Hvis dette sker, afvises hypotesen. Så længe der ikke er fundet nogen svaner i en anden farve, kan hypotesen stadig betragtes som ikke tilbagevist - dvs. som "valideret".

Falsifikationisme gælder også for lokalisering af eksistenshypoteser (også kendt som visse eksistenshypoteser): Den (generelle) hypotese "Der er hvide svaner" kan ikke testes alene. Men hvis man har opholdsstedet for en hvid svane i et rumtidsområde, er forfalskning mulig, og jo lettere jo mere begrænset er dette område. Hvis der ikke er nogen hvid svane der, kan hypotesen betragtes som tilbagevist. Omvendt følger den uforklarlige udsagn "Der er hvide svaner" fra en så bestemt eksistentiel hypotese som "Den 25. august vil der være en hvid svane i Augsburg Zoo". Imidlertid er det ikke allerede verificeret af det faktum, at forfalskningen ikke forekommer (indtil videre), så det kan tænkes, at det observerede dyr kun lignede en svane på afstand.

Yderligere former for videnskabelige hypoteser og deres verificerbarhed kan findes i Groeben og Westmeyer.

Computervidenskab (verifikation af software)

Eksamen er en af ​​de vigtigste opgaver i udviklingen af ​​komplekse, omfattende software og sikkerhedskritiske applikationer. Verifikation bruges til at bestemme, om et computerprogram svarer til dets specifikation (f.eks. Ved hjælp af Hoare-beregningen ). Bekræftelsen besvarer spørgsmålet: "Er produktet oprettet korrekt?" . Ved hjælp af verifikationen spores eksisterende fejl.

Uanset den anvendte teknologi (metoder, teknikker og værktøjer) kan verifikation ikke bevise, at det pågældende produkt er fri for mangler. Årsagen til dette er, at de krav, som kunden stiller til produktet, er i ikke-formel form og derfor ikke udgør et passende input til verifikationsprocessen. Verifikationen i datalogi er derfor at vise, at ingen fejl har fundet vej ind i udviklingsprocessen, efter at specifikationen blev oprettet. Hvis specifikationen allerede indeholder fejl, er disse ikke (nødvendigvis) bevist ved hjælp af verifikation.

Manuel / ikke-formel verifikation

Ikke-formel verifikation er i det væsentlige den dynamiske og statiske test for at finde fejl, der sneg sig ind under udviklingsprocessen. Denne type verifikation kaldes ikke-formel, fordi den ikke er baseret på matematiske beviser. Ordet manual bør ikke tages for bogstaveligt. Især med store projekter, der er udviklet over lang tid, er det almindeligt at få testene udført (delvist) automatisk ved hjælp af programmer. Evalueringen af ​​resultaterne af testkørsler udføres imidlertid ofte manuelt.

Dynamisk test

Denne type test involverer kørsel af systemet under test. I det daglige sprog forstås udtrykket "test" altid at betyde denne type test. Dynamisk test er processen med at køre testsager, der undersøger visse aspekter af systemet. Dynamiske tests kan udføres i systemets naturlige miljø eller i en simulering af det samme.

Statisk test

Statisk test er undersøgelsen af ​​et system eller en komponent uden at det udføres. Ved statisk test, ofte benævnt analyse, undersøges egenskaberne ved et system eller dets komponenter uden dets udførelse. (Designanmeldelser, kodeinspektion / gennemgang, tjeklister, formel dokumentation, kontrolflowanalyse og datastrømsanalyse);

Automatiseret / formel verifikation

Matematisk logik danner grundlaget for formel verifikation. Som i et programmeringssprog kombineres syntaks og semantik . Mens verifikation kontrollerer output fra en udviklingsfase for overensstemmelse med den foregående fase, bruges validering til at sammenligne output fra en udviklingsfase med kundernes krav. Den sætning, der bevises og modelkontrol bruges som formelle verifikationsteknikker for at øge kvaliteten af ​​softwaren.

Sætning, der beviser

Teoremet, der bevises, kan udføres på baggrund af forskellige logikker. Peled beskriver bevisteoremet ved hjælp af første ordens prædikatlogik og den mere begrænsede propositionelle logik . For at kunne bevise udsagn baseret på en specifikation kræves et bevis system, der er egnet til den anvendte logik. Korrektursystemet indeholder aksiomer og regler ved hjælp af hvilke det f.eks. B. det er muligt at bevise, at en formel er en tautologi, eller at en formel er gyldig under et bestemt, givet sæt antagelser. En automatisk sætningsprover forsøger at transformere og forenkle udsagnet, der skal bevises, gennem dygtig anvendelse af reglerne, så dens rigtighed kan bestemmes.

Modelkontrol

Modelkontrol er en anden formel teknik til verificering af software. Som teoretisk informatik lærer, er fuldautomatisk verifikation et uopløseligt problem for en bred klasse af programmer. Det kan ikke forventes, at der udvikles en verifikator, der modtager et program og en specifikation som input og bruger disse data til helt automatisk at afgøre, om programmet opfylder specifikationen. For ikke at skulle undvære support fra en computer under verificeringsprocessen i praksis kan følgende foranstaltninger træffes:
  • Begrænsning til en mindre klasse af programmer, for hvilke der findes automatiske verifikationsalgoritmer. Modelkontrol forfølger dette mål ved at begrænse det til programmer med et begrænset antal stater.
  • I stedet for at verificere hele systemet begrænser man sig til at verificere de sikkerhedskritiske dele, såsom algoritmerne eller kommunikationsprotokollerne, som programmet er baseret på.

Rumrejse

I rumrejser, som blev formet af NASA, skelnes der mellem to aktiviteter under det generiske udtryk verifikation .

kvalifikation

Formelt bevis for, at kladden opfylder alle krav til kundens krav, herunder tolerancer på grund af fremstilling, levetid, fejl osv. Og de parametre, der er specificeret i Interface Control Document ( ICD ). Afslutningen af ​​kvalifikationen er klientens underskrift på COQ (Certificate of Qualification). Metoder til kvalifikationsbekræftelse er:
  • Design review baseret på tegninger (Review of Design / RoD). En kode gennemgang udføres for software.
  • analyse
  • Test (funktioner, masse, dimensioner osv.)
  • inspektion

Hvert softwareelement testes individuelt og som en del af den overordnede konfiguration, ligesom ethvert andet element i systemet.

Formindske

Formelt bevis for, at det produkt, der skal leveres, opfylder alle kravene i kundens krav (baseret på serienummeret) og har ingen materiale- eller fremstillingsfejl. Accepteringen er baseret på bevis for den vellykkede tidligere kvalifikation (inklusive identiteten af ​​konstruktionsdokumenterne til kvalifikationsmodellen). Afslutningen af ​​accepten er klientens underskrift på COA (Certificate of Acceptance). Acceptbekræftelsesmetoder er:
  • prøve
  • inspektion

Verifikationsaktiviteterne er årsagen til de høje omkostninger ved rumudstyr sammenlignet med det samme tekniske produkt udviklet under normale industrielle forhold. Alle resultater er dokumenteret og forbliver tilgængelige for eventuelle senere nødvendige fejlundersøgelser. Mens disse regler plejede at gælde for alle niveauer ned til komponenten, forsøges der nu at reducere omkostningerne ved at bruge kommercielle komponenter til ikke-sikkerhedsrelevante enheder.

Mens rumrejser var banebrydende for udviklingen af ​​miniaturiserede elektroniske komponenter for et par år siden, er de ekstremt komplekse chips, der er tilgængelige, ikke let anvendelige til rumrejser. Deres opførsel under rumstrålingsforhold (ødelæggelse eller midlertidig forseelse) er for det meste ukendt eller kan ikke engang testes på jorden. Analyse af interaktion mellem hardware og software , som undersøger reaktionen mellem hardwarefejl og softwaren, der kører i processoren , er derfor blevet særlig vigtig for stokastiske fejl. Der er hidtil brugt store summer på NASA til at finde en kommerciel bærbar computer, der kan bruges på ISS.

Et andet højt omkostningsområde er kvalificeringen af ​​materialers langsigtede opførsel i rummet på grund af atomær ilt. I mange rumprogrammer er udstyr og materiel levetid kvalifikation meget forenklet for at holde sig inden for budgettet; for eksempel er der ingen kabler, der er certificeret i mere end tolv år. For nylig har det europæiske samarbejde om rumstandarder ( ECSS ) desværre brugt udtrykket verifikation til at henvise til de aktiviteter, der er defineret ovenfor under kvalifikation ; verifikationen af det generiske udtryk udelades, og den klare strukturering af processerne går tabt.

kvalitetssikring

Den DIN EN ISO 8402 af august 1995 punkt 2.17 middelværdi ved verifikation "Bekræftelse ved undersøgelse og tilvejebringelse af objektive beviser for, at specificerede krav er opfyldt." Denne standard refererer til kvaliteten af de organisatoriske og operationelle processer. Verifikation forstås her som en "bekræftelse i eftertid", hvorvidt eksisterende processer opnår de ønskede resultater.

ISO 8402 er trukket tilbage, men alle vilkår for kvalitetsstyring er fundet i ISO 9000 siden 2000. Den sidste version ISO 9000: 2015, afsnit 3.8.12, definerer verifikation som “bekræftelse ved at levere objektivt bevis (3.8.3), der er specificeret kravene (3.6.4) er opfyldt ". I modsætning hertil beskriver ISO 9000: 2015, afsnit 3.8.13, validering som “bekræftelse ved at levere objektiv dokumentation (3.8.3) for, at kravene (3.6.4) er opfyldt til en bestemt bestemt anvendelse eller anvendelse”.

Eksempel:

  • Bekræftelse af, at et produkt opfylder en virksomheds egen interne specifikation, fører til et verificeret produkt.
  • Bekræftelse af, at et produkt opfylder en kundespecifikation og dermed kravene til kundens brug, fører til et valideret produkt.

I en virksomhed udføres verifikation normalt først efterfulgt af validering. Frem for alt er dette korrekt forudsat at EN ISO 9001: 2008 følges, og kundens krav er fastlagt i virksomheden og fastlagt i et internt specifikationsark. Verifikationen er en kontrol af overensstemmelse med kundens krav, der er fastlagt i de interne specifikationer. Valideringen er derimod en slags feltprøve for at kontrollere, om produktet virkelig gør, hvad kunden ønsker i applikationen og derfor blandt andet er en verifikation af specifikationsarket. Et produkt, der er verificeret, men ikke valideret, bærer en stor risiko for, at brugeren eller kunden modtager et produkt, der kan have meget gode egenskaber og opfylde de interne specifikationer, men ikke opfylder kundens krav med hensyn til anvendelse.

I datalogi sammenlignes denne type verifikation med validering .

Godkendelse

Verifikation af personlige data eller protokoller er kendt som en proces med fælles underskrift eller som en suveræn godkendelseshandling . Den relaterede betegnelse godkendelse bruges også her som et synonym for bevis for identitet . På daglig tale bruges verifikation også her i teknisk dokumentation.

Eksempler på verifikation

Militære anliggender

Verifikation er betegnelsen for alle de foranstaltninger, der tjener til at overvåge overholdelse af nedrustnings- eller våbenkontrolaftaler . Verifikationsmidlerne er tekniske systemer (såsom satellitovervågning), manøvreringsobservatører og inspektører.

Resumé

Den tidlige verifikation eller verifikation af en proces eller en erklæring hjælper med at identificere fejl i god tid og til at undgå tekniske, menneskelige eller proceduremæssige kommunikationstab . Verifikation må ikke forveksles med validering .

Vurderingen af ​​indholdet af de verificerede udsagn eller data for plausibilitet eller effekt er ikke verifikationsopgaven. Det er kun et spørgsmål om at bevise en vis ægthed af selve udsagnet. Et verificeret udtryk (resultatet af et eksperiment) er således blevet kontrolleret af en tredjepart, men dets videnskabelige betydning er endnu ikke bevist. Den verificerede erklæring er derfor vigtigere end den ubegrundede påstand , men mindre vigtig end afgørende beviser . Beviset hører ikke længere til syntetisk ( empirisk ) område, men til analytisk ( teoretisk ) sandhed.

litteratur

  • Elliott Sober: Testbarhed . I: Proceedings and Addresses of the American Philosophical Association 73, 1999, s. 47-76 (PDF-version; forsvar af kriteriet).

Weblinks

Wiktionary: Verification  - forklaringer på betydninger, ordets oprindelse, synonymer, oversættelser

Individuelle beviser

  1. ↑ Burkhart Brinkmann: International ordbog for metrologi . Grundlæggende og generelle vilkår og tilknyttede vilkår (VIM) - Tysk-engelsk version ISO / IEC Guide 99: 2007, korrigeret version 2012. Red.: DIN German Institute for Standardization eV 4. udgave. Beuth Verlag, Berlin 2012, ISBN 978-3-410-22472-3 ( bipm.org - Engelsk: International Vocabulary of metrology (VIM) . 2012.).
  2. ^ N. Groeben og H. Westmeyer: Kriterier for psykologisk forskning . Juventa, München 1975, s. 107-133
  3. ↑ DIMAWEB-Interlexikon (tekniske udtryk): Die Verification dimaweb.at, 4. december 2015.
  4. ↑ Stewart Gardiner: Test af sikkerhedsrelateret software / kommunikationsnetværk, Springer-Verlag, London 1999, ISBN 978-1-4471-3277-6 .
  5. ^ A b Doron A. Peled: Software Reliability Methods / Software Engineering, Springer-Verlag 2001, ISBN 978-1-4757-3540-6 .
  6. ↑ University of Paderborn / Validering og verifikation (inklusive test, modelkontrol og sætning bevis) (PDF; 269,73 KB), 24. januar 2016