Mallintarkastus

Mallintarkastusmenetelmä kriittisten järjestelmien verifiointiin

 

VTT tutkii aktiivisesti formaalin mallintarkastusmenetelmän hyödyntämistä kriittisten järjestelmien verifioinnissa.
Tutkimushankkeiden lisäksi VTT:llä on valmiudet tehdä mallintarkastusta toimeksiantotyönä.

Mallintarkastus (Model checking) on järjestelmien verifiointiin soveltuva menetelmä, jolla voidaan tutkia täyttääkö järjestelmästä tehty formaali malli sille asetetut vaatimukset. Mallinnuksessa käytetään tyypillisesti tilakonemalleja ja tarkastettavat ominaisuudet esitetään temporaalilogiikan lausekkeina.

Mallintarkastusalgoritmit pystyvät tutkimaan kattavasti onko mallilla halutut ominaisuudet. Jos malli ei toteuta tarkastettavaa ominaisuutta, mallintarkastustyökalu esittää vastaesimerkin, joka kuvaa ominaisuuden rikkoutumiseen johtavan suoritusketjun.

Koska mallintarkastin (työkalu) huomioi järjestelmän mallin kaikki mahdolliset tilat, menetelmällä löydetään myös suunnitteluvirheet, jotka liittyvät usein epätodennäköisiin, mutta mahdollisiin tilanteisiin, joissa esim. järjestelmän käyttäjä toimii ohjeiden vastaisesti tai muistipiirit asetetaan ei-toivottuihin tiloihin. Tällaisten asioiden huomiointi perinteisin menetelmin (esim. testisuunnittelussa) on erittäin haastavaa.

VTT on tutkimus- ja asiakasprojekteissaan todennut mallintarkastusmenetelmän toimivaksi ja hyödylliseksi esim. ydinvoimaloiden järjestelmien tarkastuksessa.