Tulosta Tulosta Lähetä linkki Bookmark and Share

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.


Lisätietoja

Janne Valkonen
Erikoistutkija
020 722 6469

Antti Pakonen
Tutkija
020 722 6783

Juha Kortelainen
Tiimipäällikkö
020 722 4237

Lisätietoja

Janne Valkonen
Erikoistutkija
020 722 6469

Antti Pakonen
Tutkija
020 722 6783

Juha Kortelainen
Tiimipäällikkö
020 722 4237

Katso myös