Browsing by Subject "mallintarkastus"

Ohjelmien virheettömyys ja oikeellinen toiminta on tärkeää ohjelmistokehityksessä. Verifioinnilla voidaan estää ohjelmistojen virheet ennen kuin niihin törmätään ohjelman suorituksessa. Ohjelmien verifioinnissa ohjelmasta luodaan aluksi malli, ja tämän jälkeen malli tarkastetaan ohjelman formaalia määrittelyä vasten. Erääksi johtavaksi verifiointitekniikaksi on noussut predikaattiabstraktio, jossa ohjelmasta luodaan abstrakti malli. Tässä ohjelman suoritusta approksimoidaan joukolla valittuja predikaatteja, jotka voivat sallia suorituspolkuja joita ohjelmassa ei oikeasti ole. Predikaattiabstraktion tehokkuus perustuu siihen, että vaikka abstraktissa mallissa onkin sallivampia suorituspolkuja, abstraktio voi silti riittää sulkemaan virhetilat pois. Löyhemmät predikaatit voivat tehdä mallista tehokkaamman tarkastaa suhteessa tarkkaan malliin. Hyvien predikaattien valitseminen on huomattava haaste. Yleisin valintaan käytettävä tekniikka perustuu vastaesimerkkeihin, jotka ovat virhetilaan johtaneita suorituspolkuja. Predikaattiabstraktiossa verifioinnin tehokkuutta yritetään parantaa vähentämällä virheellisten vastaesimerkkien määrää, jotta oikeaan lopputulokseen päästään nopeammin. Tämä tehdään muun muassa vähentämällä raskasta toteutuvuuden tarkistamista, ja välttämällä käymästä uudelleen läpi jo verifioituja ohjelman osia abstraktion tarkentamisen jälkeen. CPAchecker on modulaarinen mallintarkastusohjelma. Se voi esimerkiksi ajaa predikaattiabstraktiota ja muita tekniikoita samanaikaisesti, ja yhdistää niiden tuottamaa tietoa virhetilojen poissulkemiseen. Lisäksi CPAcheckerissä standardoidut rajapinnat antavat mahdollisuuden sellaiseen vertailuun eri tekniikoiden välillä, jossa voidaan tarkasti arvioida yksittäisen tekniikan vaikutuksia ohjelman tehokkuuteen. Predikaattiabstraktioon liittyy monia tekniikoita, joilla pyritään parantamaan sen tehokkuutta. Kaikissa näissä tekniikoissa on myös heikkouksia, sillä niiden laskemiseen kuluu aikaa, eivätkä ne välttämättä vähennä tarkastusaikaa. Näiden heikkouksien vuoksi tutkielmassa on myös vertailua eri tekniikoista ja niiden tehokkuusvaikutuksista.