Ohjelmistoilla on yhä enemmän vastuuta nykyajan yhteiskunnan perusinfrastruktuurin toteutuksessa. Tämän vuoksi kysymys ohjelmistojen oikeellisuudesta on päivä päivältä tärkeämpi, kun ohjelmistovirheisiin liittyvät taloudelliset ja turvallisuusriskit kasvavat. Lisäksi paineet ohjelmistoprojektien valmistumisesta nopealla aikataululla sekä ylläpitokustannusten kurissa pitämisestä lisäävät tarvetta ohjelmakoodin abstrahoinnille ja uusiokäytölle esimerkiksi kirjastojen ja sovelluskehysten muodossa.
Erityisesti samanaikaisten ja hajautettujen järjestelmien laadunvarmistuksessa ohjelmistoalalla perinteisesti käytetyt yksittäistapauksiin perustuvat testausmenetelmät ovat usein riittämättömiä. Vakiintunutta ohjelmistoalan menetelmävalikoimaa voidaan täydentää niinsanotuilla formaaleilla menetelmillä, jotka perustuvat ohjelmiston kattavaan matemaattiseen analyysiin. Formaalit menetelmät auttavat löytämään myös harvinaisia ja vaikeasti hahmotettavia ongelmatilanteita ja lisäävät siten luottamusta ohjelmiston laatuun. Esitän esimerkkin tosielämän ohjelmistojärjestelmästä, jonka formaalista verifioinnista saatiin huomattavan positiivisia kokemuksia.
ALICE Data Point Processing Framework (ADAPRO) on avoimen lähdekoodin C++-14 ohjelmistokehys monisäikeisten (samanaikaisten) ja/tai hajautettujen palveluiden toteuttamiseen. ADAPRO:n kehittäminen sai alkunsa eurooppalaisessa ydinfysiikan tutkimuslaboratoriossa CERN:issä kesällä 2015 osana ALICE-tutkimuksen päivitysprojektia. Sovelluskehys on toteutettu käyttäen enimmäkseen standardia C++-14 kieltä ja sen standardikirjastoa, joskin eräät valinnaiset toiminnot on toteutettu Linux- ja POSIX-rajapintoja, sekä myös CERN:issä kehitettyä DIM-protokollaa hyödyntäen. Sain FUUGilta 600 euron avustuksen tutkimusprojektiin, jonka tarkoituksena oli formaalisti verifioida ADAPRO:n tärkeimmät ominaisuudet käyttäen mallintarkastus-menetelmää.
ADAPRO-sovellukset (ks. esimerkkisovellukset) perustuvat samanaikaisesti suoritettaviin säikeisiin, joita ohjataan äärellisen automaattirajapinnan kautta. Sovellusohjelmoija voi määritellä sovelluksensa logiikan olio-orientoituneesti abstraktin Thread-luokan perintään perustuen. Thread suorittaa käyttäjän määrittelemän toimenpiteen äärellisen automaatin tilasiirtymän yhteydessä. ADAPRO:n tehtävä on suorittaa tietyt rutiinit, kuten asetustiedoston luku, ulkoisten järjestelmien kanssa kommunikointi ja lokitiedoston ylläpito sovellusohjelmoijan puolesta. Lisäksi ADAPRO tarjoaa tiettyjä edistyneempiä ominaisuuksia, jotka on suunnattu pehmeiden reaaliaikasovellusten toteuttamiseen. Esimerkki tällaisesta ADAPRO-sovelluksesta on ADAPOS-järjestelmä, jota käsittelevän posterin esittelyyn ICALEPCS 2017 -konferenssissa sain aiemmin avustusta FUUG:ilta. Reaaliaikaominaisuuksien verifiointi jouduttiin rajaamaan nyt tehdyn tutkimuksen ulkopuolelle.
ADAPRO:n kaltaisen sovelluskehyksen käytössä on oleellista, että vastuunjako sovellusohjelmoijan, suoritusympäristön sekä sovelluskehyksen tarjoajan välillä on tarkasti määritelty. Eri ohjelmistokomponenttien kehittäjien on voitava tehdä oletuksia suoritusympäristön sekä muiden osapuolten toimittaman ohjelmiston oikeellisuudesta. Oletusten ja takuiden tarkkaan ja yksikäsitteiseen dokumentointiin perustuva ohjelmointisopimus on tärkeä osa ohjelmistokehyksen ammattimaista kehittämistä.
Tässä tutkimuksessa määriteltiin yhdeksän esiehtoa, joiden puitteissa ADAPRO:n tulee toteuttaa toiset yhdeksän jälkiehtoa. Esiehtoihin kuuluu mm. oletukset siitä, että käyttöjärjestelmän skeduloija on reilu, sovellusohjelmoijan toimittamat aliohjelmat aina pysähtyvät äärellisessä ajassa, sekä sovellusohjelmoijan toimittama koodi ei aiheuta muistivuotoja. Jälkiehdot puolestaan pitävät sisällään lupaukset mm. siitä, että automaattirajapintaa koskevat rajoitukset ovat voimassa kaikissa mahdollisissa suoritustilanteissa, ADAPRO ei aiheuta laittomia muistista lukemisia, ja että skeduloinnin reiluus välittyy sovellusohjelmoijan määrittelemille säikeille.
Nämä yhdeksän jälkiehtoa muotoiltiin matemaattisen logiikan avulla niinkutsutuksi ADAPRO:n teoriaksi, joka todistettiin Spin-mallintarkastajan avulla. Spinin rajoitteista johtuen ensimmäinen jälkiehto piti pilkkoa kahdeksaksi erilliseksi lauseeksi. Mallintarkastuksessa tutkittavan järjestelmän kaikki mahdolliset suoritustilanteet pyritään käymään läpi ja varmistamaan, että mallilta vaaditut matemaattiset ominaisuudet ovat aina voimassa. ADAPRO:n teoria saatiin kaikilta osin verifioiduksi sovelluskehyksen määrittelyn tasolla.
Matemaattisesti todistettu määrittely on askel oikeaan suuntaan luotettavan, skaalautuvan ja ylläpidettävän ohjelmiston kehittämisessä, mutta määrittely ei vielä takaa toteutuksen oikeellisuutta. Käytimme tutkimushankkeessamme toista mallintarkastajaa, DIVINE:ä, ADAPRO:n lähdekoodin verifioimiseen. Oikealla ohjelmalla on yleensä niin paljon mahdollisia suoritustilanteita, ettei niiden läpikäyminen kattavasti ole mahdollista rajallisten laskenta-aika- sekä muistiresurssien puitteissa. Tämä niin kutsuttu tila-avaruuden räjähdys tuli vastaan myös tässä projektissa. Näin ollen C++-toteutuksesta onnistuttiin varmentamaan vain niin kutsuttuja turvallisuusominaisuuksia käytössä olleiden resurssien puitteissa. Varmennettuihin turvallisuusominaisuuksiin kuului esimerkiksi se, ettei laittomia muistista lukemisia suoriteta, että kaikki varatut resurssit vapautetaan ajallaan ja ettei säikeiden välinen synkronointi koskaan lukkiudu. Matemaattisesti todistettu määrittely sekä huolella testattu ja osittain formaalisti verifioitu toteutus yhdessä lisäävät luottamusta ADAPRO:n laatuun, sekä helpottavat mahdollisia tulevaisuudessa tehtäviä ohjelmistopäivityksiä.
Kaiken kaikkiaan kokemuksemme mallintarkastuksen käytöstä olivat positiivisia. Onnistuimme löytämään virheitä, joita kattavat yksikkötestit, integraatiotestit ja satojen tuntien simulaatiot täydellä kuormalla ADAPOS-sovelluksilla eivät olleet onnistuneet löytämään. Nämä virheet olisivat voineet aiheuttaa katastrofaalisia virhetilanteita tuotantojärjestelmissä. Arviomme mukaan mallintarkastus on maisterivaiheen tietojenkäsittelytieteen opiskelijalta opeteltavissa muutamassa viikossa. Investointi tähän henkiseen pääomaan maksaa itsensä takaisin, kun mallintarkastuksen ja/tai muiden formaalien menetelmien käytöstä tulee osa ohjelmistotuotantotiimin päivittäistä rutiinia.
Tutkimuksessa tarkasteltiin ADAPRO-sovelluskehyksen versiota 5.0.0, joka on julkisesti arkistoitu verkossa. Yksityiskohtaisempaa tietoa löytyy edellä annettujen linkkien lisäksi ESEC/FSE 2019 -konferenssissa julkaistusta artikkelistamme:
John Lång and I.S.W.B. Prasetya. 2019. Model Checking a C++ Software Framework: A Case Study. In Proceedings of the 27th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE ’19), August 26–30, 2019, Tallinn, Estonia. ACM, New York, NY, USA, 11 pages. https://doi.org/10.1145/3338906.3340453
Lopuksi haluan kiittää Wishnua, FUUG:ia, ja muita yhteistyökumppaneitani saamastani tuesta.
John Lång
Luonnontieteiden kandidaatti, Helsingin yliopiston opiskelija
Yksi kommentti artikkeliin ”ADAPRO – matemaattisesti määritelty avoimen lähdekoodin C++ -ohjelmistokehys”