Muodollinen vahvistus

Kokeneet kirjoittajat eivät ole vielä tarkistaneet sivun nykyistä versiota, ja se voi poiketa merkittävästi 16. tammikuuta 2018 tarkistetusta versiosta . tarkastukset vaativat 10 muokkausta .

Muodollinen todentaminen tai muodollinen todiste on muodollinen todiste siitä, että tarkastuksen kohde on muodollisen kuvauksensa mukainen. Aiheena ovat algoritmit, ohjelmat ja muut todisteet.

Jo yksinkertaisenkin muodollisen verifioinnin rutiininomaisuudesta ja niiden täydellisen automatisoinnin teoreettisesta mahdollisuudesta johtuen muodollinen verifiointi tarkoittaa yleensä automaattista varmentamista ohjelman avulla .

Perustelut

Ohjelmistojen testaus ei voi todistaa, että järjestelmä, algoritmi tai ohjelma ei sisällä virheitä ja vikoja ja että se täyttää tietyn ominaisuuden. Tämä voidaan tehdä virallisella tarkastuksella.

Sovellukset

Muodollista varmennusta voidaan käyttää järjestelmien, kuten lähdekoodiohjelmistojen, salausprotokollien , kombinatoristen logiikkapiirien , sisäisen muistin sisältävien digitaalisten piirien, tarkistamiseen.

Teoreettiset perusteet

Verifiointi on muodollinen todistus järjestelmän abstraktista matemaattisesta mallista olettaen, että matemaattisen mallin ja järjestelmän luonteen välinen vastaavuus katsotaan alun perin annettuna. Esimerkiksi mallin rakentamiseen tai matemaattiseen analyysiin ja algoritmien ja ohjelmien oikeellisuuden todistamiseen.

Esimerkkejä matemaattisista objekteista, joita käytetään usein ohjelmien ja järjestelmien mallintamiseen ja muodolliseen todentamiseen, ovat:

Lähestymistavat muodolliseen todentamiseen

Muodolliseen todentamiseen on olemassa seuraavat lähestymistavat:

Todisteisiin perustuva ohjelmointi

Todistuspohjainen ohjelmointi on teknologiaa, jota käytettiin akateemisissa piireissä 1980-luvulla kehitettäessä ohjelmia tietokoneille, joilla on todisteet oikeasta - todisteista ohjelmien virheiden puuttumisesta (tämän teorian puitteissa virheet käsitellyn algoritmin ja algoritmin välisinä eroina. varsinainen ohjelman toteuttama algoritmi).

Todisteiden automaattinen tarkistus

Todistus voidaan täysin automatisoida vain hyvin pienelle joukolle yksinkertaisia ​​teorioita, joten sen automaattinen todentaminen ja sitä varten muuntaminen todennettavaan muotoon tulee tärkeäksi. Huomattava määrä käytännössä tärkeitä ongelmia, mukaan lukien esimerkiksi pysäytysongelma , on algoritmisesti ratkaisemattomia .

Tarkkuus säilytetään todentajan suorittaman todistuksen tarkistamisen yhteydessä, kun tulee tarkistaa myös todentaja, jota varten tarvitaan vielä yksi todentaja ja niin edelleen. Tuloksena oleva loputon todentajien ketju voidaan kaataa rakentamalla itsevarmentava todentaja, jolla on kyky avautua käytännölliseksi.

Katso myös

Kirjallisuus