OHJE KIRJAPAINOLLE: B5-arkin vasen- ja yläreuna kohdistetaan A4-arkin vasempaan ja yläreunaan. Näin pitäisi marginaaliksi tulla taitteen puolella noin 33 mm ja muualla noin 22 mm.
Rinnakkaisjärjestelmien algoritminen verifiointi ∗
Antti Valmari
Tampereen teknillinen yliopisto Ohjelmistotekniikan laitos
Antti.Valmari@tut.fi
Tiivistelmä
Tässä katsauksessa tutustutaan ensin siihen, miten vaikeaa rinnakkaisuutta sisältä- viä ohjelmia ja järjestelmiä on saada toimimaan luotettavasti. Sen jälkeen kerro- taan, mitä rinnakkaisjärjestelmien toiminnan automaattisella tarkastamisella käy- tännössä tarkoitetaan ja mihin se pystyy ja ei pysty. Sitten kerrotaan lyhyesti, min- kätyyppisiä kieliä on kehitetty toisaalta järjestelmän ja toisaalta siltä vaadittavien ominaisuuksien kertomiseksi verifiointiautomaatille. Loppuosassa artikkelia tutus- tutaan automaattista verifiointia vaivaavaan syvälliseen suorituskykyongelmaan ja käydään lyhyesti läpi yli puoli tusinaa keinoa sen lievittämiseksi. Asiat esitellään yleistajuisesti ilman matematiikkaa ja algoritmikuvauksia.
1 Kauhutarina
Kuvitelkaamme, että Harri Hakkerin on laadittava pankkiautomaatin ja pankin keskustietokoneen välille tietoliikenneoh- jelmisto. Pitkissä johdoissa sattuu hel- posti monenlaisia häiriöitä, joiden vuok- si sanomia voi kadota matkalla. Tehtävä- nä on laatia kumpaankin päähän ohjel- ma siten, että kokonaisuus havaitsee ka- donneet sanomat ja tarvittaessa lähettää ne uudelleen. Tällaista ohjelmistoa (tai säännöstöä, jonka mukaan se lähettää ja vastaanottaa sanomia) kutsutaan tietolii- kenneprotokollaksi. Kutsukaamme pank- kiautomaatissa toimivaa ohjelmaa “lähet- timeksi” ja pankin keskustietokoneessa toimivaa “vastaanottimeksi”.
Tietoliikenneprotokollissa käytetään
usein niin sanottuja kuittauksia. Joka ker- ta kun vastaanotin saa sanoman, se lähet- tää lähettimelle sanoman, jonka merkitys on “kiitos, kuulin viestisi”. Joka kerta kun lähetin on lähettänyt sanoman, se odot- taa kuittausta ennalta ohjelmoidun ajan, esimerkiksi yhden sekunnin. Jos kuittaus saapuu tänä aikana, lähetin toteaa sano- man välityksen onnistuneen. Jos määrä- aika menee umpeen ilman kuittauksen saapumista, lähetin lähettää sanoman uu- delleen. Tarvittaessa lähetin voi lähettää sanoman kolmannen kerran ja vieläkin useammin.
Tarinamme Harri tekee ohjelmat ja, vastuuntuntoinen kaveri kun on, testaa ne huolellisesti. Testeissä ilmenee omituinen asia: osa viesteistä menee perille kahteen
∗Artikkeli on alunperin kirjoitettu vuonna 2002 Tietojenkäsittelytieteen seuran toteutumatta jäänyttä 20- vuotisjuhlakirjaa varten.
kertaan. Siis jos Harri nostaisi tililtään 100 euroa, nosto saattaisi kirjautua kahdesti, jolloin Harrin tililtä vähennettäisiin 200 euroa!
Virhetoiminnan syyksi paljastuu seu- raava tapahtumaketju: Lähetin lähettää sa- noman. Se menee perille vastaanottimeen, joka lähettää kuittauksen. Kuittaus katoaa matkalla. Lähetin odottaa kuittausta ai- kansa ja sitten lähettää sanoman uudel- leen. Uusintakin menee perille, joten vies- ti menee perille kahdesti.
Virheen välttämiseksi vastaanottimen on jotenkin kyettävä erottamaan edellisen sanoman uusinta uudesta sanomasta. Sa- noman sisällön perusteella tätä ei voi teh- dä, koska voi olla, että sama sisältö todel- la halutaan lähettää kahdesti. Muutoinhan Harri voisi huijata pankkia nostamalla ti- liltään 100 euroa ja heti perään uudelleen 100 euroa, jolloin pankin tietokone tulkit- sisi jälkimmäisen noston edellisen uusin- naksi ja velottaisi tililtä vain 100 euroa.
Tavallisesti tämä ongelma ratkaistaan liittämällä jokaiseen sanomaan vuoronu- mero. Vastaanotin pitää kirjaa viimeksi saamansa sanoman vuoronumerosta. Se tunnistaa toistuneen sanoman siitä, että vuoronumero ei ole muuttunut viimek- si vastaanotettuun verrattuna. Itse asiassa riittää, että vuoronumeron paikalla on yk- si bitti, joka on joka toisessa alkuperäises- sä sanomassa 0 ja joka toisessa 1.
Harri teki tämän muutoksen. Nyt oh- jelmisto läpäisi perusteelliset testit. Harri vei sen pankkiin ja se otettiin käyttöön.
Puoli vuotta myöhemmin Harri sai pankista vihaisen puhelun. Hyvin pieni osa nostoista oli jäänyt kirjaamatta, eh- kä yksi kuukaudessa. Pankin asiantuntijat olivat onnistuneet osoittamaan, että vika on Harrin ohjelmistossa. Vika ilmeni eri- tyisesti perjantaisin ja palkkapäivinä.
Harrilla kesti kauan saada selville, missä vika piili. Nostotapahtumia hävisi
seuraavasti. Lähetin lähetti sanoman, ja se meni perille vastaanottimeen. Pankin tie- tokoneella oli kiirettä, koska nostosano- mia tuli tiuhaan eri automaateista, joten se kyllä lähetti kuittauksen, mutta vasta pie- nen viiveen jälkeen. Tällä välin lähettimen odotusaika kului umpeen, joten se lähet- ti sanoman uudelleen. Välittömästi tämän jälkeen kuittaus saapui lähettimelle. Auto- maatti totesi tiedon nostosta menneen pe- rille ja antoi nostajalle hänen pyytämänsä rahat.
Nostaja lähti pois, ja jonossa seuraava alkoi nostaa rahaa. Lähetin lähetti uudesta nostosta kertovan sanoman. Se hävisi mat- kalla. Edellisen sanoman uusinta oli sillä aikaa ehtinyt vastaanottimeen, joka lähet- ti siitä kuittauksen taas pienen viiveen jäl- keen. Kuittaus saapui perille. Lähetin tul- kitsi sen uudesta nostosta kertovan sano- man kuittaukseksi, vaikka se oli todelli- suudessa aikaisemman sanoman uusinta- lähetyksen kuittaus. Niinpä lähetin päätte- li tiedon uudesta nostosta menneen perille ja automaatti antoi käyttäjälle rahaa. To- dellisuudessa uusi sanoma oli kadonnut, joten tieto nostosta ei kirjautunut pankin keskustietokoneeseen.
* * *
Kertomani tarina on tietenkin tätä kirjoi- tusta varten keksitty. Oikeasti pankkiauto- maatin ja pankin välinen tietoliikenne on huomattavasti monimutkaisempi ja huo- lellisemmin varmistettu. Tarina ei silti ole pelkkää satua. Siinä kerrotun kaltaisia vir- heitä tapahtuu usein myös todellisuudes- sa. Eivätkä tällaiset ongelmat rajoitu tieto- liikennejärjestelmiin. Niitä esiintyy kaik- kialla, missä tietotekninen järjestelmä si- sältää vuorovaikutuksessa olevia omatoi- misia osia. Niitä on sattunut muun muassa puhelinverkoissa, junien kulunvalvonnas- sa, sädehoitolaitteissa ja jopa television kaukosäätimissä.
2 Rinnakkaisjärjestelmät ja niiden
virhetoiminnot
Rinnakkaisjärjestelmät (englanniksi concurrent systems) ovat tietoteknisiä järjestelmiä, joissa on ainakin kaksi yh- teistoiminnassa olevaa omatoimista osaa.
Näitä osia kutsutaan prosesseiksi. Harri Hakkerin tapauksessa niitä ovat pankki- automaatti, pankin keskustietokone ja nii- den väliset tietoliikenneyhteydet. (Min- käpä muunkaan “oma toiminto” sanoman kadottaminen on, kuin tietoliikenneyhtey- den?) Todellisessa elämässä yksittäinen laite saattaa sisältää useita prosesseja, esi- merkiksi yhden vahtimaan näppäimistöä, muutamia huolehtimaan tietoliikenteestä ja niin edelleen.
Rinnakkaisjärjestelmät ovat yleensä reaktiivisia. Reaktiivisuus tarkoittaa sitä, että järjestelmä on samanaikaisesti kor- vat höröllä useampaan kuin yhteen suun- taan. Esimerkiksi päällä oleva kännykkä on koko ajan valmiina sekä vastaanotta- maan puheluita että reagoimaan näppäi- menpainalluksiin. Reaktiivisuus vaikeut- taa järjestelmän halutun toiminnan mää- rittelyä. Mitä kännykän tulee tehdä, jos si- sään tulee puhelu kesken tekstiviestin kir- joittamisen?
Järjestelmälle voi olla määritelty mak- simiaikoja, joiden sisällä sen on ehdittä- vä tehdä tiettyjä asioita. Esimerkiksi ta- soristeyksen ohjauksen on laskettava puo- mit alas hyvissä ajoin ennen kuin ju- na saapuu paikalle. Vasteaikavaatimuksia huomioonottaen suunniteltua järjestelmää kutsutaan reaaliaikajärjestelmäksi. Reaa- liaikajärjestelmät ovat yleensä reaktiivi- sia ja rinnakkaisia. Joskus reaaliaikaisuut- ta käytetään järjestelmän sisäisenä omi- naisuutena joidenkin toimintojen luotet- tavuuden varmistamiseksi, mutta yleisesti ottaen parempana pidetään suunnitella jär-
jestelmä siten, että olivatpa ajoitukset mi- tä tahansa, järjestelmä ei tee muuta väärin kuin että se mahdollisesti myöhästyy mää- räajoistaan.
Rinnakkaisjärjestelmissä voi esiintyä kaikkia niitä virheitä mitä tietoteknisissä järjestelmissä yleensäkin. Rinnakkaisjär- jestelmissä on lisäksi vain niille tyypilli- siä virheitä. Ne aiheutuvat prosessien yh- teistoiminnan kompastelusta. Ehkä kaik- kein dramaattisin esimerkki on lukkiutu- ma (deadlock). Se tarkoittaa tilannetta, jossa jokainen prosessi odottaa, että jokin toinen prosessi tekisi ensin jotain. Luk- kiutuma voi syntyä esimerkiksi siten, että prosessi A on varannut kirjoittimen ja yrit- tää seuraavaksi varata CD-rom-aseman, ja samanaikaisesti prosessi B on varannut CD-rom-aseman ja yrittää varata kirjoit- timen. Silloin kumpikin prosessi jää tur- haan odottamaan, että toinen saisi työnsä valmiiksi ja vapauttaisi varaamansa lait- teen.
Toinen dramaattinen virhe on pillas- tuma (livelock, divergence). Se tarkoittaa tilannetta, jossa järjestelmä touhuaa lo- puttomiin, mutta ei saa mitään hyödyllis- tä aikaan. Joissakin sähköpostiohjelmissa on “lomalla”-toiminto, joka päällä olles- saan lähettää jokaiseen saapuvaan viestiin välittömästi vastauksen, jossa voi lukea vaikka “olen lomalla ja käsittelen viesti- si palattuani”. Mitä tapahtuu, jos lomal- le lähtijä kytkee toiminnon päälle ja sitten lähettää viestin kaverilleen, jolla myös on toiminto päällä? Lomalla-toiminnon en- simmäisen toteutuksen kanssa kerrotaan käyneen juuri niin. Nykyisissä toteutuk- sissa tämä on estetty esimerkiksi siten, et- tä automaattivastausta ei lähetetä samaan osoitteeseen saman vuorokauden aikana kuin kerran, vaikka sieltä tulisi useita vies- tejä.
Lukkiutumilta voi suojautua lisäämäl- lä järjestelmään ajastimia, jotka herättävät
prosessin ja ohjaavat sen tekemään jotakin muuta, kun se on odottanut liian kauan.
Pillastumilta voi suojautua laskemalla ta- pahtumien toistumiskertoja ja vaihtamal- la toimintaa, kun toistoja on kertynyt lii- kaa. Ei kuitenkaan ole helppoa keksiä, mi- tä järjestelmän tulisi tehdä, kun odotusai- ka tai toistojen määrä ylittyy. Pelkkä toi- minnan jättäminen kesken johtaa helpos- ti siihen, että järjestelmän eri osille jää eri käsitys siitä, mitä pitäisi tapahtua seuraa- vaksi. Lopputuloksena voi olla virheelli- nen kokonaistoiminto. Harrin ohjelmiston ensimmäinen versio oli laadittu sen ole- tuksen mukaan, että jos kuittausta ei tu- le, on viesti kadonnut. Jos kuitenkin vies- ti on mennyt perille ja kuittaus on kadon- nut, jää pankin tietokoneelle ja automaa- tille eri käsitys siitä, onko rahaa annettu.
Siksi lähetin lähettää viestin turhaan uu- delleen, jolloin tiliä veloitetaan kahdesti.
Harrin ohjelmisto jäi tarinassa virheel- liseksi, mutta siitä voidaan tehdä täysin vedenpitävä. Sen verran joudutaan tinki- mään, että jos yhteys katkeaa juuri kun pankin keskustietokone on lähettänyt au- tomaatille luvan antaa rahoja, ei keskus- tietokone voi olla varma, antoiko auto- maatti rahat vai ei. Tällainen tilanne voi- daan kuitenkin varmuudella havaita ja kir- jata ylös, minkä perusteella tilit voi tar- kistaa jälkikäteen. Vedenpitävä ohjelmisto on jonkin verran tarinassa kuvailtua mo- nimutkaisempi, mutta ei ylettömän moni- mutkainen.
Asian tekee hankalaksi se, että ihmis- ten on hyvin vaikeaa erottaa vedenpitävää ohjelmistoa aukollisesta. Jopa ensi näke- mältä äärimmäisen yksinkertainen järjes- telmä voi sisältää pahan virheen.
Tarkastellaan esimerkkinä järjestel- mää, jonka tehtävänä on varmistaa, et- tä jotakin yhteistä palvelua pääsee käyt- tämään vain yksi käyttäjä kerrallaan, ja vuorot jaetaan käyttäjille jotenkin oikeu-
denmukaisesti. Kirjoitin on hyvä esimerk- ki tällaisesta palvelusta: ei olisi mukavaa, jos samalle paperille tulisi rivejä vuorotel- len minun tulostuksestani ja sinun tulos- tuksestasi. Esimerkin palvelin viestii käyt- täjien kanssa siten, että jokaista käyttä- jää kohti on kaksi kaksiarvoista muuttu- jaa nimiltään “p” eli “pyyntö” ja “m” eli
“myöntö”. Järjestelmä on esitetty kuvas- sa 1.
Aluksi jokaisessa muuttujassa on arvo nolla. Kun käyttäjä haluaa käyttää palve- lua, se asettaa pyyntö-muuttujansa arvoon yksi. Palvelin antaa käyttäjälle luvan käyt- tää palvelua asettamalla käyttäjän myön- nön arvoksi yksi. Lopetettuaan palvelun käytön käyttäjä asettaa pyyntönsä nollak- si. Kun palvelin huomaa tämän, se vas- taavasti asettaa myönnön nollaksi ja, jos tähän mennessä on tullut muita pyyntöjä, antaa käyttöluvan jollekin muulle käyttä- jälle.
Vaikka en ole vielä kuvaillut periaatet- ta, jolla palvelin jakaa vuoroja jos on mon- ta pyyntöä yhtäaikaa, on järjestelmään jo rakennettu ratkaiseva virhe. Lukija voi yrittää keksiä, mikä se on. Tämä nimen- omainen virhe on helppo korjata sitten kun se on löydetty. Mutta miten voidaan olla varmoja, että järjestelmään ei jää pii- leksimään muita virheitä? Miten voidaan tietää, voiko korjattuun järjestelmään luot- taa?
Tavallinen tapa löytää virheitä järjes- telmistä on nimeltään testaus. Se on jär- jestelmän toiminnan suunnitelmallista ko- keilemista. Testaus löytää suuren osan vir- heistä, mutta ikävä kyllä osa jää aina pii- loon.
Prosessien yhteistoiminnan kompu- roinnista aiheutuville virheille on tavallis- ta, että virhe ilmenee vain, jos järjestel- män eri osissa asiat tapahtuvat ajallises- ti onnettomissa kohdissa toisiinsa nähden.
Tällaiset virheet ovat yleisiä rinnakkais-
PALVELIN A
S I A K A S 1
p1 m1
ASIAKAS2
p2 m2
A S I A K A S 3 p3
m3
ASIAKASi:n koodi pi := 1
odota kunnes mi = 1 käytä palvelua pi := 0
Kuva 1: Viallinen vuorojenjakojärjestelmä.
järjestelmissä, mutta ne ilmenevät koe- ajon tai käytön aikana harvakseltaan. Sik- si niitä on vaikea havaita testauksessa. Jos sellainen havaitaan, sen syytä on vaikea jäljittää, koska virhettä on vaikea saada toistumaan tarkempaa tutkimusta varten.
Nostotietojen hukkuminen Harri Hakke- rin ohjelmistossa on esimerkki tällaisesta virheestä. Nostoja hukkui erityisesti per- jantaisin ja palkkapäivinä, koska vain sil- loin keskustietokone oli niin kiireinen, et- tä se hidasteli riittävästi aiheuttaakseen onnettoman tapahtumaketjun.
Virheiden paljastumistodennäköisyyt- tä testauksen aikana voidaan nostaa lä- hettämällä järjestelmälle syötteitä tiuhaan tahtiin. Olettakaamme, että jonkin vir- heen esiintymistodennäköisyys normaa- lissa käyttötilanteessa on kerran miljoo- naa käyttötuntia kohti, mutta rankemman kuormituksen ansiosta virheitä sattuu tes- tauksen aikana kerran kymmenessätuhan- nessa tunnissa. Kymmenentuhatta tuntia on niin pitkä aika, että ehkä avaruus- luotaimien ohjelmistoja on varaa testata niin kauan, mutta ei tavallisia järjestelmiä.
Pankkiautomaatteja on kuitenkin Suomes-
sa lähes kaksituhatta ja nostoja tehdään vuosittain yli kaksisataa miljoonaa [17], joten käyttötunteja kertyy yhteensä mil- joonittain, ja virhe ehtii ilmetä useita ker- toja vuoden aikana.
Niinpä, vaikka testaus paljastaa vir- heitä moninkertaisella tehokkuudella ta- valliseen käyttöön verrattuna, testauksen kannalta liian harvinaisia virheitä tapah- tuu tuotantokäytössä.
3 Verifiointi
Alunperin sanalla “verifiointi” tarkoitet- tiin järjestelmän todistamista virheettö- mäksi. Vahvoja takeita virheettömyydes- tä tarvitaan, jotta jotkin järjestelmät us- kallettaisiin ottaa käyttöön. Ei ole vaka- vaa, jos joka tuhannes kännykkäpuhelu katkeaa kesken, mutta on vakavaa, jos len- tokone putoaa joka tuhannennella lennol- la!
Aikaa myöten kuitenkin huomattiin, että virheettömyyden osoittaminen on yleensä monessa suhteessa epämielekäs tavoite:
• Todellisia järjestelmiä ei koskaan saada virheettömiksi varsinkaan en- si yrittämällä. Virheellisen järjestel- män todistaminen virheettömäksi ei tietenkään voi eikä saa onnistua, ja liian yksioikoisesti sitä yrittävä ve- rifiointimenetelmä joutuu umpiku- jaan. Tästä syystä on käytännössä tärkeää, että verifiointimenetelmä pystyy myös sanomaan “järjestelmä on virheellinen” ja tuottamaan tie- toa, jonka avulla virheitä voi jäljit- tää — esimerkiksi kuvauksen virhe- tilanteeseen johtavasta tapahtuma- ketjusta. Pikkuhiljaa on alettu aja- tella, että tämä on jopa tärkeämpää kuin kyky julistaa järjestelmä vir- heettömäksi.
• Teoreettinen virheettömyys ei takaa virheettömyyttä käytännössä seu- raavasta syystä. Jotta verifiointiau- tomaatti pystyisi löytämään virheitä tai todistamaan, että niitä ei ole, sen täytyy tietää, minkälainen käyttäy- tyminen on väärää. Osa virhelajeis- ta on kaikille järjestelmille yhtei- siä — esimerkiksi täydellinen my- kistyminen kesken kaiken, mutta osa riippuu verifioitavasta järjes- telmästä — esimerkiksi onko va- lojen sytyttäminen jonain hetkenä virhe. Niinpä verifiointiautomaat- tia käyttävä ihminen joutuu taval- la tai toisella kertomaan, minkälai- nen käyttäytyminen on virheetön- tä. Kertomiseen on pakko käyttää verifiointiautomaatin ymmärtämää, usein kömpelöä kieltä. Niinpä ihmi- nen saattaa esittää ajatuksensa vää- rin. Sitäpaitsi ihmisten ajatukset ei- vät aina ole alunperinkään täysin johdonmukaisia.
• On olemassa toinenkin syy, mik- si täydellinen varmuus jää haaveek-
si. Vaikka ohjelma saataisiin veri- fioitua, sen suoritusympäristön ei voida edes periaatteessa todistaa toimivan oikein. Sähkönsyöttö voi katketa, kosmisen säteilyn hiukka- nen voi muuttaa muistin sisältöä ja niin edelleen. Käytännössä muka- na on muitakin epävarmuustekijöi- tä. Ohjelman suorittaminen esimer- kiksi vaatii, että se on ensiksi kään- netty konekieliseen muotoon. Täs- sä tarvitaan käännösohjelmia, joi- hin ei aina voi täysin luottaa. Ketjun myöhemmät lenkit jäävät siis jo- ka tapauksessa epätäydellisiksi, jo- ten ohjelman absoluuttisen virheet- tömyyden osoittamiseksi ei kannata nähdä miten paljon vaivaa tahansa.
• Parhaimpienkin tähän mennessä to- teutettujen verifiointiautomaattien suorituskyky jättää paljon toivomi- sen varaa. Poikkeustapauksia esiin- tyy, mutta pääsääntö on, että nykyi- sin ei pystytä verifioimaan oikeita ohjelmia, vaan ainoastaan niiden toimintaperiaatteet kuvaavia suun- nitelmia. Kattava verifiointi onnis- tuu rutiininomaisesti vain melko pienille järjestelmille. (Harri Hak- kerin järjestelmä on korjattunakin hyvin pieni.) Isompien järjestel- mien verifioimisessa käytetään eri- koistekniikoita, jotka joskus tehoa- vat ja joskus eivät. Sen sijaan veri- fiointia voi käyttää epätäydellisenä virheiden etsimiskeinona hyvin iso- jenkin järjestelmien tapauksessa.
Näistä syistä sanan “verifiointi” pii- riin kuuluvaksi katsotaan nykyisin pait- si ohjelmakoodin tai toimintaperiaatteen kuvauksen oikeaksi todistaminen suhtees- sa halutun käyttäytymisen kuvaukseen, myös virheiden etsiminen menetelmil- lä, jotka ainakin periaatteessa kykenisi-
vät myös oikeaksi todistamiseen. Testaus ei ole verifiointia, koska se ei edes peri- aatteessa kykene todistamaan järjestelmää virheettömäksi.
Automaattista verifiointia kutsutaan myös mallintarkastukseksi (model chec- king). Tässäkin tapauksessa sanan käyttö on laajentunut täsmällisen merkityksen- sä ulkopuolelle. Alunperin “mallintarkas- tus” on tarkoittanut sen selvittämistä, to- teuttaako annettu rakenne annetun loogi- sen kaavan. Jos vastaus on “kyllä”, niin loogikot sanovat, että rakenne on kaavan malli. Jäljempänä tässä kirjoituksessa pu- hutaan tila-avaruuksista ja aikalogiikasta.
Tila-avaruuden automaattinen tarkastami- nen aikalogiikan kaavaa vastaan on yksi verifioinnin valtavirroista ja on mallintar- kastusta sanan täsmällisessä merkitykses- sä. Mutta, kuten todettu, sanaa käytetään nykyisin lähestulkoon kaikesta toiminnas- ta, jossa jotakin vähänkin tila-avaruuden kaltaista kohdetta verrataan automaatti- sesti millä tahansa monimutkaisia ominai- suuksia ilmaisemaan kykenevällä kielellä ilmaistuun vaatimukseen.
Verifioinnista (tai mallintarkastukses- ta) on kaksi käytännön hyötyä. Ensinnäkin se kykenee löytämään käytännössä mer- kityksellisiä virheitä, jotka jäävät testauk- sessa löytymättä. Kuten edellä todettiin, tällaisia virheitä on, ja ne ovat aiheuttaneet ikäviä seurauksia.
Toiseksi, koska verifiointi ei yleensä kohdistu todellisiin järjestelmiin vaan nii- den suunnitelmiin, verifioida voidaan jo siinä vaiheessa, kun järjestelmästä on ole- massa vain suunnitelma. Virheen paljasta- minen jo tässä vaiheessa säästää huomat- tavasti, koska vältetään virheellisen suun- nitelman toteuttamisesta aiheutuva hukka- työ. Jos luotetaan vain testaukseen, ei jär- jestelmän eri osien yhteistoiminnan vir- heitä voida havaita ennen kuin osat on to- teutettu ja liitetty yhteen. Tosin on niin,
että suunnitelman verifiointi edellyttää suunnitelman esittämistä tietokoneen luet- tavassa muodossa, ja sellaista suunnitel- maa voi myös testata.
Verifiointimenetelmiä on kehitetty useisiin eri tehtäviin, mutta parhaiten ne ovat menestyneet rinnakkaisjärjestelmille tyypillisten virheiden etsimisessä ja nii- den poissaolon todistamisessa. Tämä joh- tuu toisaalta siitä, että rinnakkaisjärjestel- mille on löydetty helppokäyttöisiä ja hel- posti automatisoitavia menetelmiä, jotka eivät tehoa muualla; ja toisaalta siitä, että insinöörijärki on rinnakkaisjärjestelmien tapauksessa poikkeuksellisen epäluotetta- va. Niinpä tarpeet ja mahdollisuudet koh- taavat rinnakkaisjärjestelmissä paremmin kuin muualla.
Erityisen hyvin menetelmät ovat toi- mineet mikropiirien, kuten mikropro- sessoreiden, suunnitelmien verifioinnissa.
Tuotteessa olevat virheet ovat mikropii- rien valmistajan maineelle ja taloudelle paljon vahingollisempia kuin ohjelmisto- jen valmistajalle, mikropiireille kun ei voi lähettää jälkikäteen päivityksiä Internetin kautta. Toisaalta, sen verifioiminen, että jokin yksikkö laskee liukulukujen jakolas- kuja oikein, on mikropiirien tapauksessa sangen hyödyllinen saavutus, mutta ohjel- mien tapauksessa samantasoisen asian ve- rifiointi ei riitä pitkälle.
Rinnakkaisjärjestelmien verifioinnissa kaikkein parhaiten ovat menestyneet niin kutsutut tila-avaruusmenetelmät. Järjes- telmän tila-avaruus tarkoittaa kaikkia ti- loja, joihin järjestelmä voi joutua, sekä kaikkia näiden tilojen välisiä siirtymiä.
Kuvassa 2 on esitetty yksinkertainen esi- merkki. Tila-avaruusmenetelmien perus- ideana on muodostaa tila-avaruus osittain tai kokonaan ja analysoida sitä joko jäl- kikäteen tai muodostamisen aikana. Tila- avaruusmenetelmien etuja ja haittoja kä- sitellään yksityiskohtaisesti tämän kirjoi-
PSLK
SLK P LK PS SK PL SL PK
PSK L
K PSL S PLK
PK SL PLK S PSL K PS LK
L PSK PL SK
PSLK
Kuva 2: Suden, lampaan ja kaalin tehtävän tila-avaruus. Paimenen (P) pitää viedä susi (S), lammas (L) ja kaali (K) joen yli. Veneeseen mahtuu paimenen lisäksi korkeintaan yksi muu. Lammasta ei saa jättää suden tai kaalin seuraan ilman paimenen läsnäoloa, koska silloin susi syö lampaan tai lammas kaalin.
tuksen loppuosassa.
Jonkin verran käytetään myös teo- reemantodistusmenetelmiä. Niiden perus- ideana on todistaa järjestelmän suunnitel- man toimivuus samaan tapaan kuin mate- maatikko todistaa teoreeman, mutta päät- telytyö pyritään teettämään tarkoitukseen suunnitelluilla ohjelmistoilla, niin sano- tuilla teoreemantodistimilla.
Kokemukset ovat osoittaneet, että teo- reemantodistimen käyttäjän on formali- soitava melkoinen määrä yksityiskohtia ja ohjattava todistin kädestä pitäen todistuk- sen läpi. Matemaattisesti vaativaa ihmis- työtä tarvitaan siis paljon. Jos järjestelmä on virheellinen, ei sen virheettömyyden ilmaiseva väittämä päde, eikä niin ollen ole todistettavissa. Teoreemantodistimen käyttäjälle tilanne näkyy siten, että todis-
tusta ei saa menemään läpi vaikka kuin- ka yrittäisi. Käyttäjä saa vihjeitä virheen sijainnista analysoimalla, missä kohdassa todistus jumiutuu. Näin saatava tieto on kuitenkin epäsuoraa. Se palvelee huonos- ti verifioinnin nykyisin tärkeimmäksi kat- sottua käyttöä, eli virheiden paljastamis- ta ja jäljittämistä. Sitäpaitsi todistamisen epäonnistuminen ei takaa, että järjestelmä olisi virheellinen — voihan olla, että vikaa on vain käyttäjän todistimelle antamissa määritelmissä ja välitavoitteissa.
Näistä syistä teoreemantodistimien käyttö rinnakkaisjärjestelmien verifioin- nissa on jäänyt olennaisesti vähäisem- mäksi kuin tila-avaruusmenetelmien.
Teoreemantodistimilla on kuitenkin se kiistaton etu, että toisin kuin tila- avaruusmenetelmät, ne ovat periaatteessa
yleispätevä menetelmä, minkä vuoksi nii- tä voi käyttää joissakin tapauksissa joissa tila-avaruusmenetelmät eivät tehoa.
Teoreemantodistus ja tila-avaruuden käyttö voidaan myös yhdistää, esimerkik- si siten, että teoreemantodistin huolehtii suurista linjoista itse ja hakee yksityiskoh- taisiin kysymyksiin vastauksia mallintar- kastimelta. Jotkin tila-avaruusmenetelmät esittävät tietoa niin epäsuorassa muodos- sa, että niiden ja teoreemantodistimien ero hämärtyy. Kohdassa 6.8 käsiteltävät bi- nääripäätöskaaviot ovat esimerkki. Vielä selvempiä esimerkkejä on olemassa, ku- ten menetelmiä, jotka esittävät äärettömiä luonnollisten lukujen osajoukkoja äärel- listen automaattien avulla. Kohdassa 6.9 esitettävä rajoitettu mallintarkastus ei oi- keastaan ole tila-avaruusmenetelmä eikä teoreemantodistusmenetelmä, vaan niiden välimuoto.
Rinnakkaisjärjestelmien verifiointiin on kehitetty myös muunlaisia menetel- miä, esimerkiksi lineaarialgebraan perus- tuvia. Niiden sovellusalue on kapea, min- kä vuoksi niiden merkitys on jäänyt vähäi- seksi. Lisäksi on mainittava rinnakkaisjär- jestelmien suoritusaikoihin liittyvien omi- naisuuksien verifioimiseksi kehitetyt, tila- avaruuksiin perustuvat menetelmät. Ne muodostavat aivan oman maailmansa, jo- hon ei valitettavasti voida syventyä tässä kirjoituksessa.
4 Kuvauskielet
Kuvauskieli on kieli, jolla järjestelmä esi- tetään verifiointiautomaatille. Kuten edel- lä todettiin, suoraan ohjelmointikielel- lä esitettyjen järjestelmien automaattinen verifiointi on mahdollista vain poikkeus- tapauksissa. Ohjelmointikieltä käyttämäl- lä myös menetettäisiin mahdollisuus veri- fioida jo siinä vaiheessa, kun järjestelmäs- tä on olemassa vain suunnitelma.
Järjestelmien suunnitelmien esittämis- tä varten on kehitetty useita täsmällisiä kieliä. Käytännössä suunnitelmat esite- tään kuitenkin epätäsmällisten kaavioiden ja taulukoiden sekä luonnollisen kielen avulla, ja periaatteessa täsmällisiäkin kie- liä käytetään epätäsmällisesti, joten veri- fioinnin kannalta oleellisten tietojen poi- miminen automaattisesti suunnitelmasta on mahdotonta. Silloinkin, kun suunni- telma on täysin täsmällinen, siitä on en- nen verifiointia abstrahoitava pois suuri joukko rinnakkaisilmiöiden kannalta epä- olennaisia piirteitä, mikä vaatii ihmistyö- tä. Näistä syistä verifiointimallit esitetään tähän tarkoitukseen erityisesti suunnitel- luilla kielillä.
Rinnakkaisjärjestelmien verifiointi- mallin esittämiseen tarkoitetun kielen täy- tyy esittää selkeästi järjestelmän jakaan- tuminen rinnakkaisiin prosesseihin ja pro- sessien välinen vuorovaikutus. Prosessien sisäisestä toiminnasta on abstrahoitava mahdollisimman tarkoin pois kaikki se, millä ei ole merkitystä vuorovaikutuksen kannalta. Esimerkiksi tietoliikenneproto- kollan sisäisistä sanomista esitetään sa- noman tyyppi (dataviesti, kuittaus, . . . ) ja vuoronumero, mutta sanoman varsinainen datasisältö joko puuttuu kokonaan tai se voi saada vain kaksi tai kolme mahdollista arvoa. Vuoronumeroidenkin arvoalue voi olla pienennetty. Kaksi tai kolme datan ar- voa riittää hyvin esimerkiksi sen tutkimi- seen, voiko protokolla vaihtaa sanomien järjestystä.
Prosessien välisen vuorovaikutuksen mekanismeja on useita erilaisia. Todelli- sissa järjestelmissä käytetään paljon pus- kureita, jotka säilyttävät sanomien jär- jestyksen. Ne ovat kuitenkin verifioin- nin kannalta ongelmallisia, koska ne pys- tyvät varastoimaan paljon tietoa ja sik- si kasvattavat rajusti järjestelmän tilojen määrää. Lisäksi puskurin käyttäytyminen
silloin, kun varastointikapasiteetti loppuu kesken, voidaan määritellä monella eri ta- valla, eikä todellisen puskurin käyttäyty- mistä yleensä tiedetä. Niinpä verifiointi- mallia ei kuitenkaan saada täysin yhtäpi- täväksi todellisuuden kanssa.
Rinnakkaisjärjestelmien verifioinnis- sa käytettävissä kuvauskielissä esiintyy useita eri vuorovaikutusmekanismeja. Jot- kin tarjoavat ensisijaisesti puskurit, ku- ten CCITT:n standardoima SDL. Toiset, kuten Gerard Holzmannin ATT Bell La- boratoriossa (nykyisin Lucent Bell La- boratories) kehittämä Promela [8] tarjoa- vat monia keskenään tasa-arvoisia meka- nismeja, joista puskurit ovat yksi. (Holz- mann sai kehittämästään verifiointityöka- lusta “Spin” vuoden 2001 ACM Softwa- re System -palkinnon. Promela on Spi- nin syöttökieli. Sama palkinto on aiem- min myönnetty muun muassa Unixin, TeXin, PostScriptin, TCP/IP:n ja World- Wide Webin laatimisesta [1].)
SDL:ssä, Promelassa ja monessa muussa kielessä prosessi esitetään joko suoraan tai epäsuorasti niin sanottuna ti- lakoneena. Tilakone koostuu joukosta ti- loja ja tilasiirtymiä. Tilassa prosessi odot- taa herätettä toiselta prosessilta, järjestel- män ympäristöstä tai ajastimelta. Herät- teen saatuaan prosessi suorittaa tilasiirty- män, jonka aikana se voi lähettää herättei- tä muille prosesseille, kirjoittaa yhteiseen muistiin, laskea omien muuttujiensa avul- la ja niin edelleen.
Aivan omanlaisensa ovat lukuisat Pet- riverkkoihin perustuvat kielet. Petriver- koissa ei ole valmiina minkäänlaista pro- sessin esittämiseen tarkoitettua käsitettä.
(Sana “prosessi” kyllä esiintyy Petriverk- kokirjallisuudessa, mutta aivan eri mer- kityksessä.) Petriverkkomallin rakentaja joutuu kokoamaan sekä prosessit että nii- den väliset vuorovaikutukset alemman ta- son peruspalikoista, jotka ovat tietoa tal-
lettava paikka ja tapahtumaa ja vuoro- vaikutusta edustava transitio. Vaikka tä- mä voi kuulostaa työläältä, tilakoneiden rakentaminen paikoista ja transitioista on todellisuudessa hyvin helppoa. Petriverk- koja on tosin kritisoitu siitä, että niillä voi luontevasti matkia vain joitakin vuo- rovaikutusmekanismeja. Nykyisin käyte- tään niin sanottuja väritettyjä Petriverkko- ja [10], joilla voi kätevästi esittää järjes- telmän datasisällön sopivasti abstrahoitu- na. Petriverkoilla on havainnollinen graa- finen esitystapa (katso kuva 3). Niinpä ne ovat verifioinnissa suosittuja.
Niin sanotut prosessialgebralliset kielet, kuten ISO:n standardoima Lo- tos [3], Oxfordin yliopistossa kehitetty CSP [7, 19] ja Edinburghin yliopiston CCS [16] perustuvat synkroniseen vuo- rovaikutukseen. Siinä prosessit vuorovai- kuttavat suorittamalla tilasiirtymän yhtä- aikaa. Synkronista vuorovaikutusta käy- tetään todellisissa järjestelmissä vähän, koska sen toteuttaminen fyysisen välimat- kan yli on hyvin vaikeaa. Silti se sopii hyvin verifiointimalleissa käytettäväksi, koska sillä voi helposti matkia muita vuo- rovaikutusmekanismeja tekemällä tiedon välivarastosta (kuten puskurista) itsenäi- sen prosessin. Lisäksi synkronisen vuo- rovaikutuksen teoria on kehitetty erittäin paljon pitemmälle kuin muiden vuoro- vaikutusmuotojen teoriat, minkä ansiosta synkroniselle vuorovaikutukselle on pys- tytty kehittämään erinomaisia verifiointi- menetelmiä.
Teknillisessä korkeakoulussa Espoos- sa on käytetty Petriverkkoja rinnakkais- järjestelmien verifiointiin yli kaksikym- mentä vuotta. Monet ulkomaiset Petri- verkkotutkijat ovat ottaneet siellä kehite- tyn “Prod”-työkalun [18] käyttöönsä. Hel- singin yliopistossa on käytetty sekä tilako- nepohjaisia että prosessialgebrallisia kie- liä. Tampereen teknillisessä yliopistossa
h0i hbi l.pyyntö hv,bi
hv,bi data l.
hv,bi
hv,bi kuitt.v.
h1−bi hv,bi
viive hv,bi
h0i hbi data v.
hv,bi
hv,bi perille
hbi
hbi kuitt.l.
h1−bi hv,bi
häiriö
hi hi
hi hv,bi
hv,bi
hi data h.
h1−bi
hbi hv,bi
hi
hbi häiriö
hi
hi hi
hbi hbi
hi hv,bi kui
tt.
hv,bi h.
h1−bi hi
Kuva 3: Vuorottelevan bitin protokollan väritetty Petriverkkomalli. “l.” = lähetys, “v.” = vastaanotto ja “h.” = hylkäys virheellisen vuorottelevan bitin vuoksi. Välitettävä viesti v tulee protokollalle transitiolla “l.pyyntö” ja menee määränpäähän transitiolla “perille”.
Esimerkiksi jos oikean yläkulman paikassa onh0ija ylärivin keskimmäisessä paikassa onhv,1i, missä v on viestin sisältö, niin transitiodata h.on suoritettavissa. Se poistaa merkith0ijahv,1isekä asettaa tyhjää datakanavaa edustavaan paikkaan merkinhija kuittauksen lähettämistä edeltävään paikkaan merkinh1i. Samalla tavalladata h.voi siirtää ja muuttaa merkith1ijahv,0imerkeiksihijah0i.
algoritmisen verifioinnin tutkimus aloitet- tiin vuonna 1992. Tamperelainen työ on jatkoa silloisessa VTT:n Tietokoneteknii- kan laboratoriossa Oulussa vuonna 1984 aloitetulle tutkimukselle, joka alkoi Pet- riverkoilla, mutta on suurimman osan ai- kaa käyttänyt prosessialgebrallisia kieliä.
Tampereen ryhmän [22] saavuttamat veri- fioinnin teoriaa ja algoritmeja koskevat tu- lokset, joista osa on kehitetty yhteistyös- sä Helsingin yliopiston kanssa, on otettu maailmalla hyvin vastaan.
5 Oikean käyttäytymisen määritteleminen
5.1 Aikalogiikat
Verifiointiautomaatille on tutkittavan rin- nakkaisjärjestelmän lisäksi tavalla tai toi- sella kerrottava, minkälainen käyttäytymi- nen on virheellistä. Aluksi tyydyttiin et- simään yksittäisiin ennalta määrättyihin lajeihin kuuluvia virheitä, kuten lukkiu- tumia tai odottamatta saapuvia sanomia.
Varsin pian alettiin sekä kehittää että ottaa käyttöön muualla kehitettyjä ilmaisuvoi- maisempia tapoja määritellä virheitä. Suu- ren suosion — ja hyvillä syillä — saivat
aikalogiikat, joita israelilaiset Zohar Man- na ja vuoden 1996 Turing-palkinnon1saa- ja Amir Pnueli2, yhdysvaltalaiset Ed Clar- ke ja Allen Emerson sekä monet muut ke- hittivät 1970-luvun loppupuolelta alkaen.
Pnueli on keskittynyt lineaarisiin ai- kalogiikoihin [14], joilla määritellään ominaisuuksia, jotka järjestelmän jokai- sen yksittäisen suorituksen on täytettä- vä. Lineaarisella aikalogiikalla ei voi pu- hua vaihtoehtoisista jatkomahdollisuuk- sista suorituksen ollessa kesken. Clarken ja muiden haarautuvan ajan logiikoissa tämä on mahdollista. Lineaarinen aikalo- giikka pystyy esimerkiksi toteamaan vain, että joinakin aamuina professori juo kah- via ja joinakin teetä, mutta haarautuva ai- kalogiikka pystyy kertomaan myös, teki- kö professori valintansa kahvin ja teen vä- lillä ennen vai jälkeen kahvioon astumi- sen.
Lineaarisella aikalogiikalla esite- tyn väittämän paikkansapitävyyden tar- kastaminen rinnakkaisjärjestelmän tila- avaruudesta on työlästä (tarkasti sanoen PSPACE-täydellistä kaavan pituuden suhteen). Sen sijaan Clarken ja Emersonin kehittämän CTL:n (Computation Tree Lo- gic) [4] väittämien paikkansapitävyyden tarkastaminen on laskennallisesti help- poa. Helppous johtuu siitä, että CTL:stä on jätetty pois joitakin lineaarisen aika- logiikan piirteitä. CTL:n ilmaisuvoimasta ei silti tullut käytännön sovelluksia ajatel- len kohtuuttoman heikko, koska kyky pu- hua vaihtoehtoisista tulevaisuuksista lisää ilmaisuvoimaa. CTL onkin saavuttanut suuren suosion. Jos CTL:ään lisätään sii- tä poistetut lineaarisen aikalogiikan ope- raattorit, saadaan nimellä CTL∗ tunnettu logiikka.
Lineaarisella aikalogiikalla on kuiten-
kin omat etunsa haarautuviin verrattuna.
Jos tutkittavasta järjestelmästä löytyy vir- he, se voidaan havainnollistaa kuvailemal- la yksittäinen virheellinen suoritus. Haa- rautuvan ajan logiikassa yksinkertainen kuvailu voi olla mahdotonta. Eikä lineaa- risen aikalogiikan työläys sittenkään ole suuri ongelma, sillä lyhyillä kaavoilla työ- määrä ei kasva sietämättömäksi ja veri- fioitavat kaavat ovat yleensä lyhyitä. Niin- pä myös lineaarisen aikalogiikan suosio on suuri. Sitäpaitsi vaikka lineaarisuus ai- heuttaa tehokkuushaittaa lopullisessa tar- kastusvaiheessa, se antaa tärkeitä tehok- kuusetuja toisaalla [23]. Logiikoiden vä- linen paremmuusjärjestys ei siis ole edes tehokkuuden osalta itsestään selvä.
5.2 Ekvivalenssit ja esijärjestykset
Aikalogiikoilla määritellään yksittäisiä ominaisuuksia tyyliin “jos asiakas on teh- nyt oman osuutensa nostotapahtumasta, pankkiautomaatti antaa lopulta joko ra- haa tai virheilmoituksen” ja “tililtä ei koskaan, häiriötilanteissakaan, veloiteta enempää rahaa kuin asiakkaalle on annet- tu”. Sallittu käyttäytyminen voidaan mää- ritellä muillakin tavoilla. Eräs paljon tut- kittu mahdollisuus on määritellä toinen järjestelmä ikään kuin malliksi ja vaatia, että tutkittava järjestelmä käyttäytyy jos- sain mielessä “samalla tavalla” tai “aina- kin yhtä hyvin” kuin mallijärjestelmä. Jäl- kimmäinen vaihtoehto tarvitaan seuraa- van esimerkin havainnollistamasta syys- tä. Nimittäin, jos spesifikaatio sallii pank- kiautomaatin vastata “yhteyshäiriö” mut- ta automaatti ei koskaan vastaa niin, niin automaatti ei käyttäydy samalla tavalla kuin spesifikaatiosta tehty mallijärjestel-
1Turing-palkinto [1] on nimetty tietojenkäsittelyn teorian pioneeri Alan Turingin (1912–1954) mukaan, ja se on tietojenkäsittelytieteen alan arvostetuin palkinto.
2Pnueli kehitti logiikkansa alunperin inhimillistä päättelyä varten.
mä. Olisi kuitenkin hölmöä käyttää auto- maatin virheelliseksi julistamisen perus- teena sitä, että se ei koskaan tee spesi- fikaation sallimaa mutta epäsuotavaa toi- mintoa.
Mallijärjestelmä voi olla tavattoman paljon yksinkertaisempi kuin verifioita- va järjestelmä, koska sen ei tarvitse ol- la käytännössä toteutettavissa. Esimerkik- si pankkiautomaatti voi mallijärjestelmäs- sä käsitellä tiliä suoraan, vaikka tosimaa- ilmassa kaiken on tapahduttava epäluotet- tavan tietoliikenneyhteyden yli. Mallijär- jestelmä voidaan myös rajata yksittäiseen näkökulmaan — esimerkiksi vain kaksi asiakasta ja heidän tilinsä, vaikka todel- lisen järjestelmän on koko ajan käsiteltä- vä kaikkia tilejä. Mallijärjestelmän laati- minen voi siten olla helppoa.
Malli- ja verifioitavan järjestelmän vertaamiseksi toisiinsa on kehitetty usei- ta niin sanottuja ekvivalensseja ja esijär- jestyksiä. Ekvivalenssi tekee täsmällisek- si “samalla tavalla käyttäytymisen” käsit- teen ja esijärjestys käsitteen “käyttäytyy ainakin yhtä hyvin”.
Ekvivalenssia tai esijärjestystä käytet- täessä pitää sopia, mitkä järjestelmien ta- pahtumat otetaan vertailussa huomioon.
Esimerkiksi pankkijärjestelmän tapauk- sessa voidaan ottaa huomioon kaikki, mi- tä automaattia käyttävä asiakas voi vä- littömästi havaita, sekä hänen tilinsä sal- don muutokset. Silloin muun muassa au- tomaatin ja pankin välisen tietoliikenteen tapahtumat jätetään pois. Huomioonotet- tavia tapahtumia kutsutaan näkyviksi, ja muut tapahtumat ovat tietenkin näkymät- tömiä.
Yksinkertaisin ekvivalenssi eli jäl- kiekvivalenssi (englanniksi trace equiva- lence3) julistaa järjestelmät samanveroi- siksi, jos niiden kaikista mahdollisista
suorituksista syntyvät äärelliset näkyvien tapahtumien jonot eli niin sanotut jäl- jet ovat samat. Vastaava esijärjestys tote- aa järjestelmän olevan ainakin yhtä hy- vä kuin malli on, jos jokainen järjestel- män jälki on myös mallin jälki, mutta ei välttämättä toisinpäin. Jälkiekvivalens- si on melkein sama asia kuin kahden ää- rellisen automaatin hyväksymien kielten samuus, ja jälkiesijärjestys vastaa sitä, et- tä ensimmäisen automaatin kieli on toisen automaatin kielen osajoukko.
Näissä vertailuissa suorituksiksi las- ketaan myös suoritusten keskeneräiset al- kuosat. Tämä voi vaikuttaa omituiselta, mutta se yksinkertaistaa asioita. Jos kes- keneräisiä suorituksia ei otettaisi huo- mioon, jouduttaisiin tutkimaan sekä ää- rettömiä että päättyviä suorituksia. Asia- kashan voi palata pankkiautomaatille yhä uudelleen (asiakkaan eliniän rajallisuu- den esittäminen ei kuulu verifiointimal- lin tehtäviin!), mutta toisaalta, järjestel- män lukkiutumiset halutaan havaita, ja niitä vastaavat suoritukset ovat päättyviä.
Koska keskeneräiset suoritukset otetaan huomioon, äärettömät suoritukset tulevat riittävässä määrin huomioiduiksi kesken- eräisten alkuosiensa välityksellä, joten ää- rellisten jälkien tutkiminen riittää.
Jälkiekvivalenssi ja -esijärjestys riittä- vät sen selvittämiseen, voiko järjestelmä joutua tilanteeseen, jossa jotakin luvaton- ta on tapahtunut. Aikalogiikassa tällaisia ominaisuuksia kutsutaan turvallisuusomi- naisuuksiksi. Esimerkiksi “tililtä ei kos- kaan veloiteta liikaa” on turvallisuusomi- naisuus. Turvallisuusominaisuuksien vas- takohta on etenemisominaisuudet eli ai- dot elävyysominaisuudet, jotka voivat rik- koutua vain siten, että jotakin jää tapah- tumatta. “Jokainen nosto kirjataan lopul- ta” on etenemisominaisuus. Mikään ää-
3Verifioinnin yhteydessä saattaa törmätä myös niin sanottuihin Mazurkiewiczin jälkiin, mutta ne ovat eri asia.
rellinen jälki ei riitä todisteeksi siitä, et- tä nosto voi jäädä kirjaamatta, sillä vaikka jälki ei sisältäisi noston kirjausta, voi olla, että nosto kirjattiin hetki sen jälkeen kun jäljen nauhoittaminen lopetettiin.
Jotta järjestelmän ja mallin vertailus- sa voitaisiin ottaa huomioon myös etene- misominaisuuksia, on kehitetty jälkiekvi- valenssia monimutkaisempia ekvivalens- seja ja esijärjestyksiä. Niitä ovat kehit- täneet erityisesti prosessialgebrojen tutki- jat. Ekvivalenssilla olisi hyvä olla niin sa- nottu kongruenssiominaisuus. Se tarkoit- taa, että jos järjestelmän osan tilalle vaih- detaan ekvivalentti osa, koko järjestel- män pitää säilyä ekvivalenttina alkupe- räisen kanssa. Esijärjestyksen tapaukses- sa kongruenssiominaisuus vaatii, että jär- jestelmä ei saa huonontua siitä, että sen jokin osa korvataan paremmalla. Esimer- kiksi suksipaketin hinta ei saa nousta, jos asiakas vaihtaa siteet halvempiin. Ilman kongruenssiominaisuutta on vaikea johtaa järjestelmän osia koskevista verifiointitu- loksista koko järjestelmää koskevaa tie- toa.
Jos etenemisominaisuudet halutaan ottaa mielekkäällä tavalla huomioon, on kongruenssiominaisuus odottamattoman vaikea saavuttaa. Tämä on johtanut lu- kuisten toinen toistaan omituisempien ekvivalenssien ja esijärjestysten kehittä- miseen, jotka käsittelevät etenemisomi- naisuuksia mikä mitenkin. Aivan kuten ai- kalogiikoita, myös ekvivalensseja ja esi- järjestyksiä voidaan muodostaa sekä li- neaariselle että haarautuvalle ajalle, mikä on lisännyt sekamelskaa entisestään.
Useimmat ekvivalenssit ja esijärjes- tykset voidaan katsoa kuuluviksi kol- meen perheeseen: Robin Milnerin heik- ko havaintoekvivalenssi [16] muunnelmi- neen; estymäpohjaiset ekvivalenssit, jois- ta kuuluisin sisältyy Tony Hoaren CSP- teoriaan [7, 19] ja joihin kuuluu myös
suomalainen CFFD [28]; sekä haarautu- va bisimilaarisuus [29]. Hoare sai vuoden 1980 Turing-palkinnon, ja Milner sai sa- man kunnian vuonna 1991.
Heikko havaintoekvivalenssi ja haa- rautuva bisimilaarisuus sukulaisineen edustavat haarautuvaa aikaa. Niiden pe- rusideana on vaatia, että verrattavat jär- jestelmät voivat simuloida toisiaan. Jär- jestelmien tiloille määritellään monta–
moneen-vastaavuus siten, että kun toinen tekee jonkin asian jostakin tilastaan al- kaen, toinen voi tehdä “samanveroisen”
asian kyseisen tilan jokaisesta vastintilas- ta alkaen, minkä jälkeen järjestelmät pää- tyvät vastintiloihin. Haarautuva bisimi- laarisuus vastaa ilmaisuvoimaltaan melko tarkasti CTL-logiikkaa, ja heikko havain- toekvivalenssi on niitä heikompi.
Estymäpohjaiset ekvivalenssit perus- tuvat lineaariseen aikakäsitykseen. Ne saadaan edellämainitusta jälkiekvivalens- sista lisäämällä informaatiota niin sano- tuista estymistä (failure), joka on lukkiu- tuman yleistys. Muutakin lisäinformaatio- ta voi olla mukana, tärkeimpänä luettelo jäljistä, joiden seurauksena järjestelmä voi pillastua (katso sivu 49). Pnuelin lineaa- rista aikalogiikkaa vastaa tarkimmin suo- malainen NDFD, joka on melkein sama kuin CFFD.
NDFD ja CFFD kehitettiin ratkai- suksi CSP:n ekvivalenssin omituisuuteen, joka juontaa juurensa siitä, että CSP:n ekvivalenssi haluttiin kehittää abstraktil- la algebrallisella tasolla, vetoamatta edes tilapäisesti prosessien toiminnan sellai- siin yksityiskohtiin, jotka eivät näy ulos.
CSP:n ekvivalenssi ei säilytä mitään tie- toa järjestelmän käyttäytymisestä sen jäl- keen, kun se on suorittanut pillastuma- jäljen. Verifiointisovelluksia ajatellen tä- mä on harmillinen rajoitus. NDFD:n ja CFFD:n määritelmissä vedotaan näky- mättömiin yksityiskohtiin, mutta ne pois-
tetaan lopputuloksesta. Oxfordissa on tun- nustettu CFFD:n etu ja yritetty saada se aikaan myös CSP:n matematiikalle omi- naisin keinoin. Vuonna 2005 Roscoe jul- kaisi artikkelin [20], jossa johdettiin erit- täin paljon CFFD:n kaltainen ekvivalens- si soveltaen CSP-mäisiä keinoja syvälli- sellä tavalla. CFFD:n ja NDFD:n suhdetta CSP:hen analysoitiin Tony Hoaren eläk- keelle jäännin yhteydessä vuonna 1999 pi- detyn juhlaseminaarin eräässä esitelmäs- sä [25].
Ekvivalenssien ja esijärjestysten teo- riaa ovat Suomessa menestyksekkäästi tutkineet etenkin Jaana Eloranta, Roope Kaivola, Timo Karvi ja Martti Tienari Helsingin yliopistosta, sekä Antit Puhak- ka ja Valmari Tampereen teknillisestä yli- opistosta.
5.3 Visuaalinen verifiointi
Kuten edeltä käy ilmi, verifioitavien omi- naisuuksien määrittelemiseksi on käytet- tävissä niin voimakkaita keinoja, että omi- naisuuden ilmaiseminen ei ole kynnysky- symys. Ikävä kyllä on osoittautunut, että verifioitavien ominaisuuksien keksiminen on vaikeaa. On helppo keksiä irrallisia yk- sittäisiä ominaisuuksia, mutta on vaikea laatia verifioitavien ominaisuuksien luet- telo, jossa kaikki olennainen on mukana.
Jos on verifioitu, että tietoliikenneproto- kolla ei voi hukata eikä vääristää sanomia, on yhä mahdollista, että se voi esimerkiksi kahdentaa niitä.
Myös on vaikeaa laatia verifioitavan järjestelmän käyttäjien ja toimintaympä- ristön mallit siten, että ne eivät vahin- gossa piilota virhemahdollisuuksia. Tämä pätee erityisesti etenemisominaisuuksille.
Esimerkiksi tietoliikenneprotokollassa voi olla virhe, jonka vuoksi sanoma voi py- sähtyä matkalle, ellei perässä tule toista sanomaa, joka ikään kuin “työntää” edel- listä sanomaa edellään. Tätä virhettä ei ha-
vaita, jos tietoliikenneprotokollan asiakas mallitetaan lähettämään päättymätön jono sanomia, kuten usein tehdään.
Etenemisominaisuuksien verifiointia varten on usein tehtävä niin sanottuja rei- luusoletuksia, jotka lupaavat, että järjes- telmän eri osia suoritetaan jossain mie- lessä tasapuolisesti. Reiluusoletukset ovat usein vaikeita hahmottaa ja siksi vaikeita asettaa oikein.
Näistä syistä verifiointiautomaatteja on aina käytetty myös analyysin välinei- nä: automaatille on esitetty järjestelmän toimintaa koskevia kysymyksiä sitä mu- kaa kuin niitä tulee mieleen ilman, että verifioitavien ominaisuuksien luetteloa on muodostettu etukäteen. Tavoitteena ei ole järjestelmän osoittaminen virheettömäk- si, vaan järjestelmän toimintaa koskevan hyödyllisen palautteen saaminen vähällä vaivalla.
Viimeksi kuluneen runsaan kymme- nen vuoden aikana on erityisesti Tampe- reen teknillisessä yliopistossa tutkittu lä- hestymistapaa, joka voidaan katsoa satun- naisen kyselyn ja kattavan verifioinnin vä- limuodoksi [27]. Siinä verifiointiautomaa- tille kerrotaan vain, mitkä järjestelmän yk- sittäiset tapahtumat ovat kiinnostavia. Au- tomaatti tuottaa järjestelmän käyttäytymi- sestä eräänlaisen kyseisille tapahtumille projisoidun tiivistelmän ja esittää sen ku- vana. Tiivistelmän muodostaminen perus- tuu prosessialgebrallisiin ekvivalensseihin ja kutistusalgoritmeihin. Käyttäjän tehtä- vänä on tulkita kuva ja päättää, hyväksyy- kö hän siinä esiintyvän käyttäytymisen.
Jos käytetään lineaariseen aikaan pe- rustuvaa ekvivalenssia ja tapahtumat vali- taan sopivasti, kuva voi olla samanaikai- sesti pieni ja hyvin informatiivinen. Esi- merkiksi tietoliikenneprotokollasta saa- daan paljon tietoa muodostamalla kuva, jossa näkyvät vain sanoman välitystehtä- vän anto lähetinpäässä ja sanoman toi-
l.pyyntö
τ
perille τ
τ l.pyyntö
τ
perille τ
τ perilleτ
τ l.pyyntö
τ τ perille
l.pyyntö
perilleτ τ
l.pyyntö
Kuva 4: Vuorottelevan bitin protokollan ehjän (vasemmalla) ja Harri Hakkerin käyt- tämän (oikealla) version visualisoitu abstrahoitu käyttäytyminen. “τ”-kaaret esittävät näkymättömien tapahtumien välillisiä vaikutuksia.
mittaminen asiakkaalle vastaanotinpääs- sä. Sanomien katoamiset, kahdentumiset, matkalle pysähtymiset ja niin edelleen vihjaavat olemassaolostaan aiheuttamalla kuvaan omituisuuksia, joita käyttäjän on vaikea olla huomaamatta kuvaa tutkies- saan.
Esimerkki tästä on kuvassa 4. Kuvan oikea puoli paljastaa silkalla monimut- kaisuudellaan, että jotain on vialla. Oi- keaa puolta tutkimalla selviää, että ensim- mäinen viesti menee perille (olettaen, et- tä kuvassaτ-silmukoina ilmenevä pillastu- misen mahdollisuus vältetään), mutta sen jälkeiset lähetyspyynnöt voivat pelkkien näkymättömien tapahtumien välityksellä johtaa tilaan, jossa ainoa mahdollinen seu- raava tapahtuma on uusi lähetyspyyntö.
Toisin sanoen sanomia voi kadota.
Tämän visuaaliseksi verifioinniksi kutsutun menetelmän suurin etu on, et- tä käyttäjän ei tarvitse missään vaiheessa määritellä sallitun ja kielletyn käyttäy- tymisen välistä rajaa formaalisti. Niinpä menetelmä vaatii vähemmän koulutusta kuin tavanomainen verifiointi. Visuaali- sen verifioinnin tuottamien kuvien on ko- keissa havaittu kiinnittävän käyttäjän huo- miota sellaisiinkin käyttäytymisen piirtei- siin, joiden olemassaoloa käyttäjä ei ole aiemmin tiedostanut. Niinpä se paljastaa virheitä, jotka jäävät tavallisilta verifioin- timenetelmiltä huomaamatta, koska käyt-
täjä ei hoksaa esittää oikeaa kysymystä.
Toki käyttäjä voi tulkita visuaalisen ve- rifioinnin tuottaman kuvan väärin, mutta käyttäjä voi tehdä virheitä myös forma- lisoidessaan oikean ja väärän käyttäyty- misen välistä rajaa tavanomaiselle veri- fiointimenetelmälle. Niinpä visuaalisen verifioinnin luotettavuuden ei voi väittää olevan huonompi eikä parempi kuin taval- lisen verifioinnin.
Koska valinta oikean ja virheellisen välillä jää käyttäjän tehtäväksi, visuaali- nen verifiointi ei ole verifiointia sanan täsmällisessä merkityksessä. Menetelmän kehittäjät uskalsivat kuitenkin ottaa ni- mityksen käyttöön, sillä visuaalinen veri- fiointi käyttää samoja algoritmeja ja tuot- taa suunnilleen yhtä luotettavia tuloksia kuin tavanomainen verifiointi.
6 Tilaräjähdysongelma
6.1 Tilaräjähdysongelman syy
Edellä todettiin, että parhaidenkin tä- hän mennessä toteutettujen verifiointi- automaattien suorituskyky jättää paljon toivomisen varaa. Tähän on syvällinen syy: tyypillisistä verifiointitehtävistä voi- daan todistaa, että ne ovat laskennallises- ti varsin vaativia. Melkeinpä mikä tahansa synkronisesti vuorovaikuttavien rinnak-
kaisten tilakoneiden käyttäytymistä kos- keva kysymys on PSPACE-kova. Käytän- nössä tämä tarkoittaa, että tehtävän ratkai- semiseksi tarvittavan ajan määrä kasvaa eksponentiaalisesti tehtävän koon funktio- na.4 Myös muistin käyttö kasvaa käytän- nössä eksponentiaalisesti. Tiedetään, et- tä vähemmälläkin muistilla tultaisiin toi- meen, mutta ei tiedetä, miten sen voi- si tehdä ilman, että ajan kulutus kasvaisi kohtuuttomasti.
Muilla mallinnusformalismeilla veri- fiointikysymykset ovat yleensä ainakin yhtä työläitä. Jos vuorovaikutusmekanis- miksi vaihdetaan järjestyksen säilyttävä rajattoman kapasiteetin puskuri, muuttu- vat kysymykset algoritmisesti ratkeamat- tomiksi. Se tarkoittaa, että kysymyksen yleispätevästi ratkaisevaa ohjelmaa ei voi olla olemassa.
Nämä tulokset ovat huonoimman ta- pauksen tuloksia. Ne tarkoittavat, että jo- kainen verifiointialgoritmi on toivottoman hidas ainakin joillakin syötteillä, mutta ne eivät kerro, millä syötteillä niin käy ja on- ko niitä tiheässä vai harvassa.
Verifioinnin periaatteellinen vaikeus ilmenee eri menetelmissä eri tavoin. Teo- reemantodistimilla se ilmenee tarvitta- van ihmistyön suurena määränä. Tila- avaruusmenetelmissä se ilmenee tila- avaruuksien suurina kokoina. Jokainen järjestelmään lisättävä prosessi kasvattaa tilojen määrän tyypillisesti moninkertai- seksi. Niinpä tila-avaruuden koko kas- vaa eksponentiaalisesti prosessien määrän funktiona, ja pienelläkin järjestelmällä voi olla miljoonia, miljardeja tai vielä valta- vasti enemmän tiloja.
Tämän niin sanotun tilaräjähdyson- gelman hillitsemiseksi on kehitetty mo- nenlaisia tehokkaita keinoja, joista jotkin
ovat hyvin nerokkaita. Tässä yhteydessä voidaan esitellä niistä vain muutamia. Ra- joitettua mallintarkastusta lukuunottamat- ta kaikkia jäljempänä esiteltyjä menetel- miä ja eräitä muitakin on käsitelty perus- teellisemmin katsausartikkelissa [24].
Laskennallisen vaativuuden teoriasta seuraa sellainenkin johtopäätös, että jos NP6=PSPACE — niin kuin laajalti usko- taan, niin rinnakkaisjärjestelmissä on vir- heitä, jotka eivät voi ilmetä ennen kuin suoritus on kestänyt pitkään. Tällaisia vir- heitä on vaikea havaita etukäteen millään keinolla, mutta ne voivat ilmetä käytän- nössä, sillä esimerkiksi Internet on ollut toiminnassa jo vuosikymmeniä. Internetin tapauksessa tästä ilmiöstä ei kannata mu- rehtia, sillä siinä on varmasti yllin kyllin vähemmän eksoottisia virheitä. Avaruus- luotaimen suunnittelijan näkökulmasta ti- lanne voi olla toinen.
6.2 Symmetriat
Eräs ensi näkemältä melko ilmeinen ja sen vuoksi usein ehdotettu keino on hyödyn- tää järjestelmässä esiintyviä symmetrioita.
Ajatuksena on, että jos esimerkiksi pank- kiautomaatit ovat keskenään samanlaisia, niin verifioinnin aikana riittää tietää, että jokin niistä on antamassa rahaa, ei tarvitse tietää mikä.
Valitettavasti symmetrioiden hyödyn- tämistä vaikeuttaa se, että järjestelmien ti- lat ovat usein huomattavasti vähemmän symmetrisiä kuin järjestelmä itse. Vaikka ei tarvitse tietää, mikä pankkiautomaatti on missäkin tilassa, täytyy kuitenkin pi- tää kirjaa siitä kuinka moni on missäkin ti- lassa, mikä kasvattaa tutkittavien tilantei- den määrää. Myös verifioitava ominaisuus saattaa rikkoa symmetrian: ei riitä havai- ta, että jonkin tilin saldo pieneni, vaan sal-
4Vaikka on hyviä syitä uskoa, että kaikki PSPACE-kovat tehtävät vaativat eksponentiaalisesti aikaa, ei asiaa ole onnistuttu sitovasti todistamaan. Laskennallisesti vaativien tehtävien teoriaa on käsitelty mukavalla tavalla kirjassa [5].
don pitää pienetä sillä tilillä, jolta nosto tapahtui. Lisäksi symmetrioiden hyödyn- täminen hävittää eräiden ominaisuuksien verifioinnissa välttämätöntä tietoa. Näiden vaikeuksien vuoksi symmetrioiden käytön idea on pirstoutunut moneksi eri menetel- mäksi, joista muutamia on esitelty kirjois- sa [10, osa 2] ja [4].
Symmetrioista saatava hyöty riip- puu symmetrian määrästä. Peilisymmet- ria pystyy enimmillään puolittamaan tilo- jen määrän. Ympyräsymmetria jakaa tilo- jen määrän parhaassa tapauksessa proses- sien määrällä. Se on tilojen määrän eks- ponentiaalisen kasvun rinnalla vain pie- ni parannus, mutta saattaa kuitenkin riit- tää kasvattamaan suurimman verifioitavan järjestelmän kokoa muutamalla prosessil- la. Symmetriasta saadaan todella suurta hyötyä vasta, jos järjestelmässä on joukko prosesseja, jotka ovat täysin samanveroi- sessa asemassa sekä suhteessa toisiinsa et- tä suhteessa muuhun järjestelmään. Näin on esimerkiksi tähtikytkentäisessä järjes- telmässä, jossa on yksi keskusasema tai palvelin, jolla on useita asiakkaita, joiden välillä ei ole suoria kytkentöjä.
Rajoitetun sovellettavuutensa ja hei- kohkon kutistustehonsa vuoksi symmet- riamenetelmää ei ole toteutettu läheskään kaikissa verifiointityökaluissa. Symmet- riat eivät silti ole jääneet vajaalle käytöl- le, sillä ihmiset ovat hyviä hyödyntämään niitä epäformaalisti verifiointimalleja laa- tiessaan.
6.3 Datariippumattomuus
Symmetrioiden kanssa hieman samankal- tainen menetelmä on datariippumatto- muuden hyödyntäminen. Sen lähtökohta- na on havainto, että monet rinnakkais- järjestelmät varastoivat tai siirtävät dataa ilman, että katsovat sen sisältöä. Niin- pä, jos järjestelmä toimii oikein jollakin data-arvolla, se toimii oikein millä tahansa
data-arvolla. Näin ollen riittää, että järjes- telmää verifioitaessa on käytössä muuta- ma erisuuri data-arvo. Enemmän kuin yk- si data-arvo tarvitaan, jotta data-alkioiden katoaminen, kahdentuminen ja vaihtumi- nen voitaisiin havaita.
Datariippumattomuus voi ilmetä myös siten, että yksittäisillä data-arvoilla on merkitystä järjestelmän käyttäytymiselle, mutta tutkittava ominaisuus ei riipu sii- tä, kuinka monta eri data-arvoa on käytös- sä, kunhan niitä on vähintään jokin määrä.
Esimerkiksi eräistä tietoliikenneprotokol- lista voidaan yksinkertaisen, helposti au- tomatisoitavan päättelyn ja tavallisen au- tomaattisen verifioinnin yhdistelmällä to- distaa, että protokollan käyttäjilleen tuot- tama palvelu ei riipu uudelleenlähetysten määrästä. Toisin sanoen, käyttäytyminen ei riipu siitä, kuinka monta kertaa proto- kollan lähetin yrittää sanoman lähetystä ennen kuin se luovuttaa ja ilmoittaa, että sanomaa ei saada läpi — kunhan se yrit- tää ainakin kerran.
Järjestelmän toiminta voi olla riip- pumatonta paitsi data-arvoista tai nii- den määrästä, myös samanlaisten, jonkin säännöllisen hahmon mukaisesti toisiin- sa kytkettyjen prosessien määrästä. Täl- löin riittää verifioida järjestelmä jollakin pienellä samanlaisten prosessien määräl- lä, mutta tulokset pätevät mille tahan- sa isommalle määrälle. Muuttujat voidaan tulkita prosesseiksi, joten tavallinen tau- lukko on erikoistapaus säännöllisen hah- mon mukaisesti toisiinsa kytketyistä pro- sesseista.
Datariippumattomuutta hyödynnetään yleensä ihmistyönä: verifiointityökalun käyttäjä päättelee riittävän data-arvojen määrän (tai prosessien määrän tai taulu- kon koon) ja karsii data-arvot (tai pro- sessit tai taulukon alkiot) muutamaan jo verifiointimallia laatiessaan. Datariippu- mattomuuden käyttöä on pyritty automa-
tisoimaan toisaalta johtamalla teoreemo- ja, joista riittävän arvojen määrän voi suo- raan katsoa (kirjan [19] luvussa 15.3 on esimerkkejä), ja toisaalta kehittämällä au- tomaattisia abstrahointimekanismeja, jot- ka karsivat liiat data-arvot kun järjestel- män kuvausta käännetään verifiointityö- kalulle. Molemmilla alueilla on edistyt- ty, mutta ainakin vielä nykyisin tulokset ovat verifiointityökalun käyttäjän näkö- kulmasta keskeneräisiä. Ehkä pisimmällä on G. Holzmannin Lucent Bell Laborato- riossa kehittämä järjestelmä, jossa ennalta määrätyn koodauskäytännön mukainen ja vuorovaikutustoiminnot ennalta määrätty- jä aliohjelmia kutsumalla toteuttava C- kielinen tietoliikenneohjelma käännetään käyttäjän antaman vihjekokoelman avulla verifiointimalliksi [9].
Datariippumattomuuden hyödyntämi- nen käsityönä on luontevaa siksikin, että verifiointimallin laatija joutuu melkein ai- na abstrahoimaan, muuten verifiointityö- kalu tukehtuu jo ensi vaiheessa. Niinpä on luontevaa ensin verifioida järjestelmä yhdellä data-arvolla tai toistuvalla proses- silla tai taulukon alkiolla. Jos se onnis- tuu, määrää kasvatetaan kahteen, kolmeen ja niin edelleen, kunnes verifiointityöka- lu tukehtuu tai uutta tietoa järjestelmästä ei enää saada. Näin voi tehdä ja tehdään, vaikka järjestelmä ei olisikaan datariippu- maton. Silloin verifiointia ei saada täysin kattavaksi, mutta, kuten edellä todettiin, täysin kattava verifiointi on joka tapauk- sessa yleensä liian vaativa tavoite.
Monen tämänkaltaisen tekniikan yh- täaikaisesta käytöstä on oppikirjamainen esimerkki kirjan [19] luvussa 15.3.3 sekä kirjoituksessa [26]. Suomeksi alaa on kä- sitelty kirjoituksessa [21].
6.4 Tila-avaruuden vaiheittainen muodostaminen
Edellä puhuttiin prosessien vertaamises- sa käytettävien ekvivalenssien ja esi- järjestysten kongruenssiominaisuudesta.
Kongruenssiominaisuus tekee mahdolli- seksi järjestelmän tila-avaruuden rakenta- misen vaiheittain siten, että jaetaan jär- jestelmä osiin, muodostetaan jokaisel- le osalle tila-avaruus, kutistetaan kunkin osan tila-avaruus ekvivalenssin määritte- lemät ominaisuudet säilyttäen ja lopuksi yhdistetään osatila-avaruudet kokonaisuu- den tila-avaruudeksi. Lopputulos voi ol- la valtavan paljon pienempi kuin aito tila- avaruus, mutta on silti sen kanssa ekviva- lentti ja niin ollen tuottaa samat vastaukset verifiointikysymyksiin. Osan tila-avaruus voidaan muodostaa samalla periaatteella jakamalla osa vielä pienempiin osiin.
Tällainen tila-avaruuden vaiheittai- nen muodostaminen on osoittautunut erit- täin tehokkaaksi keinoksi vastustaa tilarä- jähdystä. Sitä käytettiin verifiointityöka- lussa tiettävästi ensimmäisen kerran Rans- kassa 1980-luvun lopulla, ja sen jälkeen sitä on tutkittu paljon varsinkin Euroo- pan eri maissa Suomi mukaan lukien. Sen ehkä ainoa merkittävä heikkous on, että sen yhteydessä on vaikea käsitellä asian- mukaisesti aikalogiikassa yleisesti käytet- tyjä reiluusoletuksia (katso sivu 61). To- sin Antti Puhakan väitöskirjassa vuodelta 2004 saavutettiin tällä saralla edistystä.
Klassisessa ohjelmien oikeaksi todis- tamisessa käytetään usein apuna niin sa- nottuja invariantteja. Invariantti on väit- tämä, josta voidaan tietyllä periaatteella päätellä, että se on aina voimassa, kun oh- jelman suoritus on tietyssä kohdassa. In- varianttien muodostaminen on usein työ- lästä (mikä on yksi pääsyy siihen, että teoreemantodistimien käyttö verifioinnis-
sa on työlästä).
Tila-avaruuden vaiheittaisessa muo- dostamisessa voidaan käyttää apuna raja- pintaprosesseja. Ne muistuttavat hieman invariantteja sikäli, että niiden avulla ve- rifiointityökalun käyttäjä voi esittää väit- tämän, jonka hän uumoilee olevan aina voimassa tietyssä kohdassa järjestelmää.
Tällaisen väittämän voimassaolo riippuu usein järjestelmän osan vuorovaikutukses- ta muiden osien kanssa. Niinpä ympäris- töstään irrotettu järjestelmän osa voi jou- tua tilanteisiin, joissa väittämä ei päde.
Tämä voi kasvattaa sen tila-avaruutta mer- kittävästi. Tällaiset tilanteet leikkautuvat pois sitten kun osan tila-avaruus yhdiste- tään muiden osien tila-avaruuksiin. Silloin on kuitenkin jo myöhäistä: niiden muo- dostamisen vaiva on jo nähty.
Tämä turha työ voidaan välttää ra- japintaprosesseja käyttämällä. Verifiointi- työkalu voi pienentää osan tila-avaruutta jo sitä muodostaessaan jättämällä pois ti- lanteet, joissa rajapintaprosessin esittämä väittämä on rikkoutunut. Jos väittämä pi- tää paikkansa koko järjestelmän tasolla, niin verifiointityökalu tuottaa samat lopul- liset tulokset kuin ilman rajapintaproses- sia, mutta vähemmällä vaivalla. Jos väit- tämä ei pidäkään paikkaansa, verifiointi- työkalu havaitsee lopuksi että näin on ja varoittaa käyttäjää, että verifiointitulokset ovat sen vuoksi puutteelliset. Käyttäjän ei siis tarvitse tietää etukäteen, pitääkö väit- tämä paikkansa.
Vaiheittaisesta tila-avaruuden muo- dostamisesta on kehitetty muunnelma, jo- ka symmetriamenetelmän tavoin hyödyn- tää sitä tosiasiaa, että monessa järjestel- mässä on useita keskenään samanlaisia osia — esimerkiksi monta samanlaista pankkiautomaattia. Siinä järjestelmään li- sätään samanlaisia osia yksi kerrallaan, kunnes järjestelmän käyttäytymisen pro- jektio tietyille näkyville tapahtumille ei
enää muutu. Nämä näkyvät tapahtumat sisältävät tarkasteltavien ominaisuuksien kannalta olennaisten tapahtumien lisäk- si rajapinnan, johon osat lisätään. Tällä muunnelmalla on useita kertoja onnistuttu verifioimaan järjestelmä siten, että tulok- set pätevät riippumatta samanlaisten osien määrästä. On siis verifioitu kokonainen ääretön järjestelmäperhe rajallisella työl- lä. Tämä menetelmä voidaan katsoa esi- merkiksi datariippumattomuudesta.
Vaiheittaista tila-avaruuden muodos- tamista muunnelmineen on käsitelty oppi- kirjamaisesti artikkelissa [26].
6.5 Lennosta verifiointi
Vaikutukseltaan jonkin verran rajapinta- prosessien kaltainen on lennosta verifioin- tina tunnettu lähestymistapa. Lennosta ve- rifiointi tarkoittaa, että tarkastettava omi- naisuus otetaan tavalla tai toisella huo- mioon jo tila-avaruuden muodostamisen aikana ja muodostaminen lopetetaan heti kun havaitaan virhe.
Jos esimerkiksi Harri Hakkerin pank- kiohjelmiston mallista verifioidaan len- nosta, että jokaista nostoa vastaa saman- suuruinen saldon väheneminen ja päinvas- toin, niin tila-avaruuden muodostaminen lopetetaan heti, kun nosto jää kirjaamat- ta ensimmäisen kerran. Tavallisessa veri- fioinnissa tila-avaruuden muodostaminen ei loppuisi tähän vaan jatkuisi kenties hy- vinkin pitkään, tuottaen sekä tiloja, jot- ka edustavat tapahtumien kehitystä vir- heen jälkeen, että tiloja, jotka edustavat niitä vaihtoehtoisia tapahtumakulkuja, joi- ta ei ollut vielä tutkittu kun virhe ilmeni ensimmäisen kerran. Virheen ensimmäi- sen ilmenemisen jälkeen tutkittavia tilo- ja on monessa tapauksessa huomattavasti enemmän kuin sitä ennen tutkittavia. Veri- fioimalla lennosta säästetään siis huomat- tavasti aikaa ja muistia verrattuna siihen,
että tila-avaruus muodostetaan ensin ko- konaan ja virheet paljastetaan tutkimalla valmista tila-avaruutta.
Osa lennosta verifioinnin tekniikoista kykenee ainakin osittain estämään niiden tilojen muodostamisen, joilla ei ole mer- kitystä tutkittavan ominaisuuden kannalta.
Jos esimerkiksi halutaan tutkia, käynnis- tääkö ydinvoimalan säätöohjelmisto var- masti turvajärjestelmän ennen reaktoria, niin tutkimista ei tarvitse jatkaa tilois- ta, joissa turvajärjestelmä on käynnistet- ty. Osa lennosta verifioinnin menetelmis- tä tekee tämän automaattisesti tutkitta- van ominaisuuden ilmaisevan mallijärjes- telmän tai aikalogiikan kaavan pohjalta.
Verifiointimallin tekijäkin voi toki ohjel- moida tällaisen rajoituksen suoraan mal- liinsa, mutta automatiikka tekee sen var- memmin oikein.
Lennosta verifiointiin on lukuisia eri tekniikoita. Monien yksittäisten ominai- suuksien, kuten lukkiutumattomuuden, tarkastaminen lennosta verifioimalla on tietysti helppoa. Prosessialgebrojen ta- pauksessa esijärjestykset yhdistettynä Ed Brinksman vuonna 1987 ehdottamaan kanonisten testaajien teoriaan tarjoavat luontevan keinon monimutkaisten ominai- suuksien verifiointiin lennosta. Lineaari- sen aikalogiikan kaavoina annetut väit- tämät voi kääntää niin sanotuiksi Büchi- automaateiksi, joita on kohtalaisen help- po käsitellä tila-avaruuden muodostami- sen aikana, kuten Moshe Vardi ja Pier- re Wolper ehdottivat vuonna 1986. Heille myönnettiin vuoden 2000 Gödel-palkinto tästä ja eräistä tähän liittyvistä, teoreetti- semmista keksinnöistään [6]. Heidän ni- missään on muitakin automaattisen veri- fioinnin keskeisiä tuloksia.
6.6 Tiivistetty tila
bittivektorin indeksinä
Tilaräjähdystä voi hillitä myös valitse- malla tila-avaruudelle tavallisesta poik- keava esitystapa. Gerard Holzmann ehdot- ti vuonna 1987 tila-avaruuden esittämis- tä suurena bittitaulukkona, jota indeksoi- daan tilan kuvauksesta hajautusfunktiol- la muodostetulla tiivistelmällä [8]. Aluksi taulukon kaikki bitit ovat nollia. Sitä mu- kaa kuin tiloja löytyy, niitä vastaavat bitit asetetaan ykköseksi.
Koska taulukon indeksi on muodostet- tu hajautusfunktiolla tiivistämällä, mon- ta eri tilaa kuvautuu samalle bitille. Täs- tä seuraa, että tila saatetaan tulkita jo löy- detyksi, vaikka se on todellisuudessa uusi.
Käyttäytymisen jatko kyseisestä tilasta al- kaen jää silloin tutkimatta. Holzmannin menetelmä ei siis takaa tulosten katta- vuutta, eikä ole verifiointimenetelmä sa- nan normaalissa merkityksessä.
Holzmannin menetelmän kyky löytää virheitä on kuitenkin samantapainen kuin verifiointimenetelmien. Se on hyvä mene- telmä silloin, kun tavoitteena on täydel- lisen kattavuuden sijasta tutkia niin pal- jon kuin tietyn ennalta määrätyn muis- tin rajoissa on mahdollista. Holzmannin menetelmä valikoi tutkimatta jäävät tila- avaruuden alueet melko satunnaisesti. Li- säksi menetelmä käyttää sille annettua muistia todella tehokkaasti: jos bittitau- lukko täyttyy edes puoliksi, muistia tarvi- taan vain kaksi bittiä tutkittua tilaa koh- ti! On tosin huomattava, että kuten tila- avaruusmenetelmät yleensä, myös Holz- mannin menetelmä tarvitsee merkittäviä määriä lisää muistia pitääkseen kirjaa kes- keneräisestä työstä.
Koska Holzmannin menetelmä jät- tää melko mielivaltaisesti tiloja tutkimat- ta, voisi luulla, että sitä ei voi käyt- tää monimutkaisten, useista tiloista ja niiden keskinäisistä suhteista riippuvien
