2/2015

Luotettavan tietokoneohjelman tekeminen on mahdollista, mutta ei kannata

Antti Valmari

 

Meneekö hissi ylös kun painaa Ylös-nappulaa, vai alas, koska samaan aikaan joku painoi nappulaa alemmassa kerroksessa? Tällaisia ohjelmiston ja laitteiston yhteistoiminnan ongelmia pohtii työkseen CAV 2014 -palkinnon saaja, professori Antti Valmari TTY:n matematiikan laitokselta.

 

Jos tietokoneohjelmien jatkuvista virhepäivityksistä haluttaisiin eroon, keinot siihen kyllä löytyvät. Mutta se ei ole ohjelmistoyrityksille taloudellisesti kannattavaa, väittää professori Antti Valmari.

Tietokoneohjelmien päivitykset paikkaavat niistä löytyneitä turvallisuusaukkoja. Usein ne keskeyttävät työskentelyn koneella juuri silloin, kun on kiire. Niin tuttua?

– Tutkijat osaisivat tehdä ohjelmistoista niin luotettavia, että niitä ei tarvitsisi päivittää vähän väliä, väittää professori Antti Valmari TTY:n matematiikan laitokselta.

– Ohjelmistoyrityksillä ei kuitenkaan ole halua ottaa sellaisia menetelmiä käyttöön, koska ne olisivat ainakin alkuvaiheessa kalliita ja aikaa vieviä. Se viivyttäisi tuotteen saamista markkinoille ja edellyttäisi toimintakulttuurin muutosta. Päivitysten lähettäminen netin kautta on ohjelmistoyrityksille helpompaa ja halvempaa.

Mikropiirien valmistajilla tilanne on toinen. Jos lukkiutumattomien jarrujen mikropiiristä löytyy vika, joutuvat autojen valmistajat kutsumaan miljoonia autoja huoltoon osan vaihtamiseksi. Se tulee erittäin kalliiksi, joten mikropiirien valmistajat ovat hyvin motivoituneita pyrkimään virheettömyyteen.

– Lentokoneiden valmistajilla on halu tehdä luotettavia ohjelmistoja, jotta lentäminen olisi turvallista. He eivät kuitenkaan voi poiketa kovin paljoa ohjelmistoalan yleisestä kulttuurista, koska toisella tavalla koulutettuja ohjelmoijia on niukasti tarjolla. Siltä varalta, että tietokoneohjaus pettää, useimpia matkustajalentokoneita voi ohjata myös siitä riippumattomasti, Valmari sanoo.

Virheet löytyvät testaamista tarkemmilla keinoilla

Testaamisella pyritään löytämään tietokoneohjelmien virheet. Testattaessa käydään läpi erilaisia vaihtoehtoisia tilanteita yksi reitti kerrallaan. Ongelmana on Valmarin mukaan se, että kaikkia vaihtoehtoja ei voi testata etukäteen.

Tietokoneavusteinen verifiointi (Computer-Aided Verification, CAV) on tutkimusala, jossa pyritään löytämään testaamista tarkempia automaattisia keinoja tietokoneohjelmien ja mikropiirien virheiden löytämiseen.

CAV Award 2014

Tietokoneavusteinen verifiointi (Computer-Aided Verification, CAV) on tutkimusala, jossa pyritään löytämään testaamista tarkempia automaattisia keinoja löytää tietokoneohjelmien ja mikropiirien virheet.

  • CAV Award on vuonna 2008 alalle perustettu, vuosittain jaettava palkinto.
  • Viime vuoden palkinto jaettiin 19. heinäkuuta 2014 Wienissä osana Vienna Summer of Logic -tapahtumaa.
  • Antti Valmari oli yksi neljästä vuoden 2014 palkinnon saajasta.
  • Muut palkinnon saajat olivat Patrice Godefroid Yhdysvalloista, Doron Peled Israelista ja Pierre Wolper Belgiasta.
  • Godefroid, Peled ja Valmari tekivät palkitut keksintönsä toisistaan riippumatta vuoden 1990 molemmin puolin. Wolper oli Godefroid’n väitöskirjan ohjaaja. Sittemmin Valmari oli yksi Godefroid’n vastaväittäjistä. Monet muutkin alkoivat kehittää samoja ajatuksia. Niistä kasvoi tutkimusala, joka on aktiivinen tänä päivänäkin.
  • 10 000 dollarin palkintosumma jaettiin tasan palkittujen kesken.
 

– Tietokoneavusteisessa verifioinnissa ei yritetä tutkia yksittäisiä reittejä, vaan vaihtoehtojen verkostoa eli niin sanottua tila-avaruutta kokonaisuudessaan. Vaihtoehdoista muodostuu verkosto, jossa on monta reittiä samaan päämäärään, Valmari selittää.

Hän on kehittänyt menetelmiä, joilla voidaan tutkia ohjelmiston osien tai ohjelmiston ja laitteiston yhteistoimintaa ja varmistaa, että piileviä virheitä ei ole. Työstään hän sai heinäkuussa 2014 kansainvälisen CAV Award -palkinnon.

Yhteistoiminta kompuroi

– Klassinen esimerkki yhteistoiminnan virheestä on tilanne, jossa johtajan puoliso ostaa tiistai-illaksi teatteriliput, kun taas johtajan sihteeri lupaa asiakkaalle, että johtaja vie asiakkaan tiistai-iltana ravintolaan. Johtajalle tulee kaksi varausta samalle ajankohdalle.

Valmari kertoo esimerkin siitä, miten ohjelmiston ja laitteiston yhteistyö voi kompuroida.

– Kaivinkone saattaa katkaista pankkiautomaatin ja pankin tietokonesalin välisen kaapelin sen jälkeen, kun pankin tietokone on antanut automaatille luvan antaa rahaa. Silloin pankin tietokone ei voi tietää, antoiko pankkiautomaatti rahaa vai ei.

– Tietoliikenneyhteyden toimivuutta ei voida taata, mutta kehittämilläni menetelmillä voidaan varmistaa, että pahimmassakaan yhteyshäiriössä pankki ei veloita tiliä, jos automaatti ei antanut rahaa, Valmari summaa.

Teksti: Leena Koskenlaakso
Kuva: Mika Kanerva

 
Kerro kaverille
Säätiöpääoman tuotoilla rakennetaan tulevaisuutta
Säätiöpääoman tuotoilla rakennetaan tulevaisuutta
2/2015
Säätiöpääoman tuotoilla rakennetaan tulevaisuutta
TTY osallistuu CERNin uuden hiukkaskiihdyttimen käyttövarmuuden suunnitteluun
TTY osallistuu CERNin uuden hiukkaskiihdyttimen käyttövarmuuden suunnitteluun
2/2015
TTY osallistuu CERNin uuden hiukkaskiihdyttimen käyttövarmuuden suunnitteluun
VTT ja TTY mukaan fuusioenergian robotiikkasopimukseen
VTT ja TTY mukaan fuusioenergian robotiikkasopimukseen
2/2015
VTT ja TTY mukaan fuusioenergian robotiikkasopimukseen
Aurinkosähköä älyverkkoon
Aurinkosähköä älyverkkoon
2/2015
Aurinkosähköä älyverkkoon
Nanosellusta uusia markkinoita
Nanosellusta uusia markkinoita
2/2015
Nanosellusta uusia markkinoita
Joukkoistaminen mullistaa teollisten yritysten toimintatapoja
Joukkoistaminen mullistaa teollisten yritysten toimintatapoja
2/2015
Joukkoistaminen mullistaa teollisten yritysten toimintatapoja
LUMATE-tiedekerhosta wau-fiiliksiä
LUMATE-tiedekerhosta wau-fiiliksiä
2/2015
LUMATE-tiedekerhosta wau-fiiliksiä
Pelitutkija kehittää uusia menetelmiä matematiikan oppimiseen
Pelitutkija kehittää uusia menetelmiä matematiikan oppimiseen
2/2015
Pelitutkija kehittää uusia menetelmiä matematiikan oppimiseen
Tiedon valoon!
Tiedon valoon!
2/2015
Tiedon valoon!
Marianne Poulsen: Otatko vastuun omasta työstäsi ja pysytkö uteliaana?
Marianne Poulsen: Otatko vastuun omasta työstäsi ja pysytkö uteliaana?
2/2015
Marianne Poulsen: Otatko vastuun omasta työstäsi ja pysytkö uteliaana?
Uudet puhdastilat TTY:lle
Uudet puhdastilat TTY:lle
2/2015
Uudet puhdastilat TTY:lle

Tampereen teknillinen yliopisto on teknologisen kehityksen tiennäyttäjä sekä tutkimusmaailman ja elinkeinoelämän yhteistyökumppani. Yliopistosta valmistuu haluttuja osaajia yhteiskunnan eri aloille.

Käyntiosoite:
Korkeakoulunkatu 10,
33720 Tampere

Postiosoite:
PL 527, 33101 Tampere

Puhelinvaihde:
03 311 511
ma–pe kello 8–16.15
kesällä ma–pe 8–15.45

Virallinen sähköpostiosoite:
tty.asiointi@tut.fi