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 .
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.
Muodollista varmennusta voidaan käyttää järjestelmien, kuten lähdekoodiohjelmistojen, salausprotokollien , kombinatoristen logiikkapiirien , sisäisen muistin sisältävien digitaalisten piirien, tarkistamiseen.
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:
Muodolliseen todentamiseen on olemassa seuraavat lähestymistavat:
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).
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.