Tehtävä:
Vuorottelevan bitin protokolla
Lyhyt MathCheck-ohje (uuteen välilehteen)
Tässä tehtävässä tutustutaan pikkuisen siihen, miten vaikeaa on suunnitella luotettavia tietoliikennejärjestelmiä, ja miten äärelliset automaatit voivat olla siinä avuksi. Tarvitaan paljon muutakin kuin mitä tässä kerrotaan, joten tämä tehtävä antaa asiasta liian yksinkertaisen kuvan. Tässä esitettävät asiat antavat kuitenkin suuntaa.
- Huono tietoliikenneprotokolla
- Vuorotteleva bitti
- Ikuisen silmukan välttäminen
- Lopuksi
Huono tietoliikenneprotokolla
![[huonon protokollan rakenne]](ABP_rakenne.png)
Oheinen kuva havainnollistaa yhtä perusongelmaa, joka
tietoliikennejärjestelmien suunnittelijoiden on täytynyt ratkaista.
Tavoitteena on välittää viestejä kuvan vasemmasta reunasta oikeaan reunaan.
Kuvassa on esimerkin vuoksi kahta eri viestiä: a ja b.
Lähetyspaikasta vastaanottopaikkaan on epäluotettava kanava (kuvassa D), joka
toisinaan välittää viestin perille kunnolla, mutta toisinaan vääristää sen tai
hukkaa kokonaan.
Esimerkiksi salamanisku voi häiritä sekä kaapeleissa että radioteitse kulkevia
viestejä.
Myös vastakkaiseen suuntaan on epäluotettava kanava (kuvassa K).
Tässä tehtävässä käsitellään viestien katoamisen ongelmaa. Viestien vääristymisen varalle on kehitetty omat, täysin toisenlaiset tekniikkansa. On myös muita ongelmia, joille on omat ratkaisunsa. Esimerkiksi Internetissä viesti pilkotaan osiin, jotka saattavat kulkea eri reittejä. Ne voivat saapua perille väärässä järjestyksessä. Tässä tehtävässä oletetaan, että kanavassa viestit voivat kadota, mutta mitään muuta epätoivottua niille ei voi siellä tapahtua. Ne eivät esimerkiksi vääristy, kahdennu tai tule perille väärässä järjestyksessä.
Lähetyspaikassa sijaitseva käyttäjä lähettää viestin matkaan tapahtumalla a tai b. Lähetys- ja vastaanottopaikassa on ohjelmat L ja V, jotka keskustelevat keskenään kanavien D ja K välityksellä viestien välittämiseksi luotettavasti vastaanottavalle käyttäjälle. Järjestelmä luovuttaa viestin sille tapahtumalla aV tai bV. Harmaa laatikko edellä olleessa kuvassa ilmaisee sitä, että käyttäjät näkevät vain nämä neljä tapahtumaa a, b, aV ja bV. Tätä näkökulmaa kutsutaan järjestelmän tuottamaksi palveluksi.
Kanavaa D kutsutaan datakanavaksi. Kun L on saanut lähettävältä käyttäjältä viestin a tai b, se lähettää sen datakanavaa pitkin tapahtumalla aL tai bL. Jos …datakanava ei hukkaa sitä, se tulee V:lle tapahtumalla …aD tai bD, jonka jälkeen V antaa sen vastaanottavalle käyttäjälle tapahtumalla …aV tai bV.
Tämänkaltaista säännöstöä, joka kertoo miten erillisten osien on tehtävä yhteistyötä, kutsutaan protokollaksi. Käymme nyt läpi esimerkin protokollamme toiminnasta. Jotta sinun olisi helpompi seurata mitä tapahtuu, tästä klikkaamalla saat L:n, D:n, V:n ja K:n NFA:t sekä yleisrakenteen näkyviin palautelaatikkoon. Järjestelmän tilat ilmoitetaan neljällä numerolla järjestyksessä L:n tila, D:n tila, V:n tila ja K:n tila. Esimerkiksi jos L on alkutilassaan, D on oikeassa reunassa, V on alareunassa ja K on oikeassa reunassa, niin tila on …1342.
Aluksi kaikki ovat tilassa 1 eli koko järjestelmän tila on 1111. Kirjoita paperille tai tekstitiedostoon ”1111”. Tapahtuma a siirtää L:n tilasta 1 tilaan 2. Koska a ei ole muiden osien aakkostoissa, ne pysyvät tilassa 1. Siksi järjestelmän tila on nyt 2111. Kirjoita ”a 2111”, niin että kaikkiaan lukee ”1111 a 2111”, ja jatka kirjoittamista esimerkin etenemisen mukaan. Seuraavaksi aL siirtää L:n tilasta 2 tilaan 3 ja D:n tilasta 1 tilaan 2 muiden osien pysyessä paikoillaan. Järjestelmän tila on nyt …3211.
Nyt on kolme vaihtoehtoa mitä voi tapahtua seuraavaksi: …aD vie tilaan 3121, …εL vie tilaan 2211 (Käytämme alaindeksiä kertomaan, minkä osan ε-kaaresta on kyse.) tai …εD vie tilaan 3111. Uudelleenlähetyksen havainnollistamiseksi valitsemme niistä viimeksi mainitun. Seuraavaksi …εL vie tilaan 2111, jossa on jo oltu. Nytkin …aL vie tilaan 3211. Tästä jatkamme siten, että sanoma pääsee perille, siitä lähetetään kuittaus ja sekin pääsee perille ja luetaan. Siis seuraavat tapahtumat ja tilat ovat …aD …3121 …aV …3141 …kV …3112 …kK …1111.
Paperilla tai tiedostossa pitäisi lukea tämä1111 a 2111 aL 3211 εD 3111 εL 2111 aL 3211 aD 3121 aV 3141 kV 3112 kK 1111. Kun siitä poimitaan käyttäjille näkyvät tapahtumat eli joukkoon {a, b, aV, bV} kuuluvat tapahtumat, saadaan a aV. Siis yksi a lähetettiin, se meni yhtenä kappaleena perille, ja järjestelmä palasi alkutilaan. Tämä on toivottua käyttäytymistä.
Tarkastelemme seuraavaksi tilojen ja tapahtumien jonoa 1111 b 4111 bL 5311 bD 5131 bV 5141 kV 5112 εK 5111 εL 4111 bL 5311 bD 5131 bV 5141 kV 5112 kK 1111. Siitä poimittu käyttäjille näkyvien tapahtumien jono on tämäb bV bV. Onko se toivottua käyttäytymistä? vastausEi ole. Yhteen kertaan lähetetty b tuli perille kahtena.
Protokolla voi myös jäädä ikuiseen silmukkaan tällä1111 a 2111 aL 3211 εD 3111 εL 2111 aL 3211 εD 3111 εL 2111 aL 3211 εD 3111 εL 2111 … tavalla. Luvussa Ikuisen silmukan välttäminen mietimme, mitä tälle voi tehdä.
Protokolla voi jopa edetä alkutilasta alkutilaan siten, että lähetettyjen viestien joukossa on yksi b, mutta yhtään b:tä ei tule perille. Miten? vastaus1111 a 2111 aL 3211 aD 3121 aV 3141 εL 2141 aL 3241 kV 3212 kK 1211 aD 1121 aV 1141 b 4141 bL 5341 εD 5141 kV 5112 kK 1111.
Seuraavissa luvuissa korjaamme nämä viat.
Vuorotteleva bitti
Jos L:n lähettämä viesti saavuttaa V:n mutta V:n takaisinpäin lähettämä kuittaus katoaa tai viivästyy, L ei saa tietoa viestin perillemenosta ja siksi lähettää sen uudelleen. Jos myös uusi lähetys menee V:lle saakka, edellisen luvun V antaa myös sen käyttäjälle, jolloin käyttäjä saa saman viestin kahdesti. Tämän estämiseksi V:lle täytyy antaa jokin keino erottaa, onko L:ltä tullut viesti uusi viesti vai aikaisemman viestin uudelleenlähetys.
Vuorottelevan bitin protokollassa tämä tehdään vuorottelevalla bitillä (alternating bit). L liittää jokaiseen V:lle lähettämäänsä viestiin ylimääräisen bitin, jonka arvo on 0 tai 1. Alkuperäiseen viestiin liitettävän bitin arvo on eri kuin edelliseen alkuperäiseen viestiin liitetyn bitin arvo, ja uudelleen lähetettävään viestiin liitettävän bitin arvo on sama kuin saman viestin ensimmäiseen lähetykseen liitetyn bitin arvo. V muistaa viimeksi käyttäjälle välittämäänsä viestiin liitetyn bitin arvon, ja sen perusteella välttää välittämästä saman viestin toiseen kertaan. Myöhemmin käsiteltävästä syystä myös kuittauksiin liitetään bitti, jonka arvo on sama kuin kuitatun viestin bitin. Aluksi vuorottelevan bitin arvo on 0.
Mikä menisi pieleen, jos V ei lähettäisi kuittauksia niistä L:n lähettämistä viesteistä, joissa on väärä bitin arvo? vastausL lähettäisi samaa viestiä uudelleen loputtomasti, koska ei koskaan saisi kuittausta sillä bitin arvolla, jota se odottaa. Protokolla pyörisi hyödyttömässä silmukassa ikuisesti.
Tästä klikkaamalla saat L:n, D:n, V:n ja K:n näkyviin. Tämä protokolla on yksisuuntainen vuorottelevan bitin protokolla. Vuorottelevan bitin protokollan (kaksisuuntaiseen tiedonsiirtoon sovellettuna) julkaisivat K.A. Bartlett, R.A. Scantlebury ja P.T. Wilkinson vuonna 1969. Alkuperäisjulkaisu ja lehden siihen samalla julkaisema palaute ovat yhteensä vain 3 sivua pitkät. Ne löytyvät täältä.
Jollei kuittauksissa olisi vuorottelevaa bittiä, protokolla hukkaisi sanomia. Sen osoittamiseksi korvaamme …kV0:n ja kV1:n kV:llä sekä …kK0:n ja kK1:n kK:lla, ja käytämme K:sta vain tiloja 1 ja 2. Anna esimerkki tilojen ja tapahtumien jonosta, joka vie alkutilasta alkutilaan, jossa tapahtuu ainakin yksi b, ja jossa ei tule perille yhtään bV:tä. vihje 1Luvun 1 lopussa näytettiin, miten b voidaan hukata. vihje 2Kun protokolla on hukannut b:n, lähetä a:ta ja vältä ε-kaaria, niin protokolla päätyy lopulta alkutilaansa. vastaus1111 a 2111 aL0 3211 aD0 3121 aV 3141 εL 2141 kV 2152 aL0 3252 kK 6251 aD0 6141 b 9141 bL1 (10)541 εD (10)141 kV (10)152 kK 1151 a 2151 aL0 3251 aD0 3141 kV 3152 kK 6151 a 7151 aL1 8451 aD1 8161 aV 8181 kV 8112 kK 1111
![[ihanteellinen palvelu, kapasiteetti 1]](ABP_palvelu.png)
Jos kuittauksissa on vuorotteleva bitti, niin protokollan tuottama palvelu on
oheisen NFA:n mukainen.
Niinpä siltä osin kuin asiaa voi tutkia äärellisillä automaateilla, tämä
protokolla on virheetön.
Se on todettu sekä automaattisesti että ihmisvoimin päättelemällä.
Kuva ei kuitenkaan kerro koko totuutta, sillä NFA:t eivät pysty paljastamaan kaikenlaisia virheitä. Ne eivät huomaa virheitä, joissa ulos ei tule mitään väärää, mutta oikeat viestit lakkaavat kulkemasta. Luvussa Huono tietoliikenneprotokolla esitetty protokolla saattaa jäädä ikuiseen silmukkaan. Vuorottelevan bitin protokolla on altis samalle ongelmalle. Seuraavassa luvussa ratkaisemme sen niin hyvin kuin sen voi ratkaista. Sitä ennen päättelemme, miksi vuorottelevan bitin protokolla ei koskaan anna ulos väärää viestiä.
L:ssä on koko ajan vuorotteleva bitti. D:ssä joko ei ole mitään tai on yksi viesti, jossa on vuorotteleva bitti. V:ssä …on koko ajan vuorotteleva bitti. K:ssä …joko ei ole mitään tai on yksi viesti, jossa on vuorotteleva bitti. Osoitamme, että näiden bittien muodostamassa jonossa on koko ajan korkeintaan yksi epätyhjä kohta, jossa bitin arvo on eri kuin edellisessä epätyhjässä kohdassa. Jono voi olla esimerkiksi 1100, 0ε00 tai 0ε1ε (ε tarkoittaa tyhjää kanavaa), mutta ei voi olla 1101 eikä 010ε.
Lause 1 L:n, D:n (jos epätyhjä), V:n ja K:n (jos epätyhjä) bittien muodostama jono on koko ajan muotoa 0⋯0, 0⋯01⋯1, 1⋯1 tai 1⋯10⋯0.
Todistus. Käytämme invarianttipäättelyä, eli osoitamme, että väite on voimassa aluksi, eikä mikään, mitä protokolla tekee, voi saada väitettä pois voimasta.
Aluksi jono on …0ε0ε.
D:n, V:n ja K:n NFA:ista on helppo katsoa, että mikään niistä ei koskaan välitä viestiä eteenpäin eri bittiarvolla kuin oli viimeisimmässä sen saamassa viestissä. L ottaa uuden bittiarvon käyttöön vasta kun …se on saanut K:sta kuittauksen edellisellä bittiarvolla. Juuri ennen kuin L lukee tämän kuittauksen, L:n ja K:n bittiarvot ovat …samat.
Jos jonossa olisi sillä hetkellä molempia bittiarvoja, siinä olisi sekä kohta, jossa 0:n perässä on 1 että kohta, jossa 1:n perässä on 0. Koska …tarkoituksemme on osoittaa, että L:n toiminto ei voi saada väitettä pois voimasta, meillä on lupa olettaa, että väite on sillä hetkellä voimassa. Siksi …jonossa ei voi olla kahta vaihdoskohtaa, joten jonossa on vain yhtä bittiarvoa. Kun L ottaa uuden bittiarvon käyttöön, syntyy yksi vaihdoskohta, mutta edellä mainitusta syystä se on jonon ainoa. □
Olemme osoittaneet, että jonossa on korkeintaan yksi kohta, jossa bitin arvo vaihtuu. Seuraavaksi päättelemme tätä hyödyntäen, että protokolla ei koskaan anna ulos väärää viestiä.
Lause 2 V antaa kunkin alkuperäisen viestin ulos korkeintaan kerran, ja jos alkuperäinen viesti hukkuu, niin V ei anna enää mitään ulos.
Todistus. L käsittelee käyttäjältä saamansa viestit yhden kerrallaan. L ei ota seuraavaa viestiä käsittelyyn ennen kuin edellinen on käsitelty. Kunkin viestin L käsittelee seuraavasti. L lähettää sen kertaalleen ja sen jälkeen uudelleen ja uudelleen, kunnes L saa kuittauksen samalla bittiarvolla.
Jos yksikään L:n lähettämä viestin kopio ei saavu V:lle, protokolla jää ikuiseen silmukkaan, jossa ei tapahdu mitään hyödyllistä. Tässä tapauksessa viesti katoaa, mutta V ei kuitenkaan anna ulos mitään väärää, koska se ei anna ulos enää mitään.
Jos ainakin yksi niistä saapuu V:lle, niin V …välittää käyttäjälle niistä ensimmäisen, jonka se saa, ja vain sen. Tässä tapauksessa viesti tulee käyttäjälle oikein ja vain yhtenä kappaleena. Sen jälkeen protokolla joko jää ikuiseen silmukkaan jossa käyttäjälle ei anneta enää mitään (kuinka?)Näin käy jos kaikki kuittaukset häviävät, tai kaikki tai yhtä vaille kaikki dataviestit häviävät, yhtä vaille kaikki kuittaukset häviävät, ja L ei lue sitä yhtä vaan siirtyy aina uudelleenlähetykseen., tai siirtyy tilaan, jossa se on valmis seuraavan viestin välittämiseen. □
On helppo nähdä, että protokolla ei voi joutua tilanteeseen, missä yksikään osa ei voi tehdä mitään. Jos D ei ole tilassa 1, niin se voi siirtyä ε-kaarta pitkin tilaan 1. Jos L on tilassa 1 tai 6, niin se voi tehdä a:n ja b:n. Jos se on tilassa 2, 4, 7 tai 9, niin joko D ei ole tilassa 1, jolloin D voi tehdä jotakin; tai …L voi tehdä aL0:n, bL0:n, aL1:n tai bL1:n. Jos L on tilassa 3, 5, 8 tai 10, niin …L voi siirtyä ε-kaarta pitkin.
Ikuisen silmukan välttäminen
Jos jompikumpi kanava on kauan poikki ja jokin viesti on välittämättä, niin vuorottelevan bitin protokolla pyörii silmukassa kunnes yhteys taas toimii. Useissa sovelluksissa olisi parempi, että L antaisi periksi muutaman lähetysyrityksen jälkeen ja antaisi lähettävälle käyttäjälle virheilmoituksen. Siksi kehitämme monimutkaisemman protokollan lisäämällä tapahtumat ok ja err, joilla L kertoo käyttäjälle, saiko se kuittauksen vai luovuttiko.
Kun L on palauttanut err ja myöhemmin tulee uusi a tai b, kumpaa vuorottelevan bitin arvoa L:n tulee käyttää sille? vastausKumpikaan vaihtoehto ei toimi aina oikein. Olettakaamme, että edellinen viesti lähetettiin bitin arvolla 0 ja että 0 oli siinä tilanteessa oikea arvo. Jos se ei koskaan saapunut V:lle asti, niin mitä V tekee saadessaan seuraavaksi viestin bitin arvolla 0? Entä bitin arvolla 1? Katso jatkovastaus 1. Jos se saapui V:lle asti, niin mitä V tekee saadessaan seuraavaksi viestin bitin arvolla 0? Entä bitin arvolla 1? Katso jatkovastaus 2. jatkovastaus 1Koska 0 oli oikea bitin arvo edellistä viestiä lähetettäessä, V odotti silloin viestiä bitin arvolla 0. Koska sellaista ei tullut, V odottaa yhä viestiä bitin arvolla 0. Sellaisen se välittää käyttäjälle ja bitin arvolla 1 varustettua viestiä ei välitä. Molemmissa tapauksissa se kuitenkin lähettää kuittauksen sillä bitin arvolla, joka viestissä oli, jotta L saisi tiedon, että sen uudelleen lähettämistä ei tarvitse jatkaa. jatkovastaus 2Koska V sai edellisen viestin, V odottaa seuraavaksi viestiä bitin arvolla 1. Niinpä V käsittelee nollan ja ykkösen päinvastoin kuin edellisessä vastauksessa: välittää 1-viestin käyttäjälle mutta 0-viestiä ei välitä.
Tämä ongelma ratkeaa ottamalla käyttöön yhteyspyyntöviestit y0 ja y1, joissa on vuorotteleva bitti, mutta ei hyötykuormaa. V ei välitä kummastakaan mitään käyttäjälle ja vastaa molempiin kuittauksella, jossa on sama bitin arvo. Kun L ei tiedä kumpaa bitin arvoa sen pitäisi käyttää, se lähettää yhteyspyyntöviestin viimeksi käyttämällään bitin arvolla. Jos siihen tulee kuittaus, L vaihtaa bitin arvoa ja lähettää dataviestin.
Koska häiriöt voivat olla tilapäisiä, saattaa olla edullista laittaa L lähettämään yhteydenpyyntöviesti muutamaan kertaan ennen luovuttamista. Vastaavasti jos yhteys saadaan, L:n kannattaa lähettää dataviesti muutamaan kertaan ennen luovuttamista. Piirrämme kuviin kuitenkin vain yhden yrityksen kummastakin, jotta kuvista ei tulisi liian isoja. Samasta syystä käytämme tässä luvussa vain yhtä viestiä a (siis b jää pois).
Kuvan piirtäminen tämän protokollan tuottamasta palvelusta on hankalaa siksi, että lähetin voi antaa periksi ennenaikaisesti, jolloin ensin tulee err ja vasta sitten aV. Voi jopa käydä niin, että lähetin ehtii siinä välissä ottaa uuden a:n ja ehtii vastata sillekin err.
Lopuksi
Järjestelmän käyttäytyminen voidaan tutkia automaattisesti muodostamalla tuloautomaatti ja analysoimalla sitä tavalla tai toisella. Voidaan esimerkiksi lisätä protokollaan käyttäjiä edustava DFA, joka lähettää viestejä ja tarkastaa, että ulos tulee kulloinkin se mikä viimeksi lähetettiin. Se menee lopputilaan silloin ja vain silloin, kun ulos tulee väärä viesti. Protokollan muiden osien kaikki tilat muutetaan lopputiloiksi. Jos protokolla ei koskaan anna ulos mitään väärää, tuloautomaatin hyväksymä kieli on ∅. Jos protokolla antaa ulos jotain väärää, tuloautomaatista voidaan lukea tilojen ja tapahtumien jono, joka johtaa virheeseen.
Haluttu käyttäytyminen voidaan myös ilmaista loogisina kaavoina. Osataan tehdä ohjelmia, jotka tarkastavat, toteuttaako tuloautomaatti kaavat. Jollei toteuta, nytkin tarkastin antaa tilojen ja tapahtumien jonon, joka johtaa virheeseen. Voidaan myös laatia vertailukohde DFA:na ja testata, käyttäytyykö tuloautomaatti vähintään yhtä hyvin kuin se. Järjestelmä voi käyttäytyä vertailukohdetta paremmin esimerkiksi siten, että vertailukohde sisältää err-haaran, mutta järjestelmä ei koskaan valitse sitä.
Tällaiset menetelmät ovat kehittyneet hyvin pitkälle. Yksi niiden ongelma on se, että tuloautomaatit ovat usein valtavia. Tuloautomaattia ei kuitenkaan yleensä tarvitse muodostaa kokonaan, vaan tunnetaan menetelmiä muodostaa pienempiä automaatteja, jotka säilyttävät tiedon järjestelmän mahdollisesta virheellisestä käyttäytymisestä. Tässä on vuosikymmenten aikana edistytty huimasti. Valitettavasti ongelma ei todennäköisesti tule koskaan täysin ratkeamaan siksi, että virheiden etsiminen järjestelmästä on PSPACE-kova tehtävä. Tämä syy vaikuttaa kaikkiin virheiden etsimisen menetelmiin, ei siis pelkästään tuloautomaatteja käyttäviin.
Toinen ongelma on se, että järjestelmältä halutun palvelun tunnistaminen on uskomattoman vaikeaa. Kattavaa ja virheetöntä kuvausta siitä, mitä sen pitää tehdä ja mitä se ei saa tehdä, ei useinkaan osata laatia. Jos järjestelmä tekee jotain hölmöä, niin sen tapahduttua osataan kyllä sanoa, että ei sen näin pitänyt tehdä. Vaikeampaa on kieltää ne hölmöydet, joita järjestelmä ei vielä ole tehnyt.
Vuonna 2017 sattunut tapaus on hyvä esimerkki tästä vaikeudesta. Pyörätuolissa istuva henkilö halusi maksaa 74,50 euron hintaiset talvikengät antamalla 4,50 euroa rahaa ja Kelan myöntämän maksusitoumuksen, jonka yläraja oli 70 euroa. Kassa kieltäytyi, koska ohjeissa luki, että ostos ei saa ylittää maksusitoumuksen arvoa. Ohjeen tarkoitus ei ollut kieltää tällaista yhdistelmämaksua, vaan varmistaa, että kauppa ei hyväksy maksusitoumusta sen ylärajaa suuremmasta summasta. Tapaus oli asiakkaalle kamala ja sai kaupan hukkumaan vihapostiin. Tapauksessa ei ollut kyse ohjelmointivirheestä vaan siitä, että ihmisten noudatettavaksi tarkoitettuun ohjeeseen ei osattu kirjoittaa sitä mitä haluttiin.
Toisinaan on mahdollista korvata tuloautomaatissa muut kuin ulospäin näkyvät tapahtumat ε:lla, muodostaa pieni saman kielen hyväksyvä NFA, ja näyttää se kuvana. Kuvasta voidaan tulkita järjestelmän käyttäytymistä silloinkin kun ei etukäteen osata sanoa tarkasti, miten sen tulisi käyttäytyä. Kuva saadaan automaattisesti, mutta se on harvoin niin pieni, että ihminen pystyy tulkitsemaan sitä.
Ongelmaksi on muodostunut myös se, mitä tarkoitetaan, kun sanotaan, että kaksi järjestelmää tuottaa saman palvelun. Siltä osin kuin on kyse siitä, voiko järjestelmä tehdä mitään väärää, se ei ole ongelma: järjestelmät tuottavat saman palvelun jos ja vain jos niiden ulospäin näkyviin tapahtumiin rajoitetut NFA-esitykset hyväksyvät saman kielen. Tilanne mutkistuu kuitenkin hyvin paljon, jos halutaan tutkia jättääkö järjestelmä tekemättä asioita jotka sen pitää tehdä. Tämä on johtanut syvällisiin matemaattisiin tutkimuksiin, joilla ei ensi näkemältä luulisi olevan mitään tekemistä järjestelmien virheiden etsimisen kanssa. Hyvä esimerkki siitä on tämä nykyisin ilmainen kirja.
Näistä ongelmista huolimatta menetelmät pystyvät tarkastamaan järjestelmiä huolellisemmin kuin mihin ihminen yleensä pystyy päättelemällä. Siellä, mihin ne soveltuvat, ne löytävät virheet kattavammin kuin mihin testaaminen pystyy. Sielläkään, mihin ne soveltuvat, ne eivät korvaa testaamista, vaan täydentävät sitä, koska ne ovat testaamista paljon raskaampia. Koska tietokoneen sisällä olevan mikropiirin vaihtaminen ehjään on hankalaa, mikropiirien valmistajat käyttävät tämänkaltaisia menetelmiä varmistamaan, että mikropiirit ovat mahdollisimman virheettömiä. Ohjelmistovalmistajat eivät käytä, koska ohjelmien ei tarvitse olla mahdollisimman virheettömiä, sillä ne voidaan päivittää netin kautta.