Mallintarkastus kriittisten automaatiojärjestelmien suunnittelun tueksi

Mallintarkastus on formaali menetelmä kriittisten järjestelmien verifiointiin ja validointiin (V&V). Simulointi ja testaus perustuvat aina tiettyjen ennalta määriteltyjen sekvenssien ja kombinaatioiden läpikäyntiin, mutta mallintarkastuksen avulla voidaan kattavasti tarkastaa, voiko jostakin järjestelmästä tehty malli käyttäytyä eitoivotulla tavalla, vasten järjestelmän vaatimuksia. Analyysin kattavuuden vuoksi ns. piileviä suunnitteluvirheitä on käytännön sovelluksissa löytynyt myös järjestelmistä, joita on jo tarkastettu testaamalla ja simuloimalla. Suomessa mallintarkastuksen soveltuvuutta mm. automaatiosuunnittelun arviointiin on tutkittu kansallisessa ydinvoimalaitosten tutkimusohjelmassa SAFIR:ssa. Onnistuneista tutkimuspiloteista on nopeasti siirrytty käytännön sovelluksiin. VTT on soveltanut menetelmää niin voimalaitos-, tehdas-, kone- kuin sähköautomaationkin kohteisiin. VTT:n toimesta mallintarkastusta on tähän mennessä useimmiten sovellettu suunnittelu- ja V&V-prosessin jo läpikäyneiden järjestelmien riippumattomaan arviointiin. Virheiden löytäminen näin myöhäisessä vaiheessa on kuitenkin erittäin kallista. Koska menetelmä on laskennallisesti tehokas, ja analyysi siten nopea suorittaa, herää kysymys, miksei mallintarkastusta ole otettu osaksi suunnittelun työkaluja ja prosesseja. Vaikka mallintarkastukseen käytetyt työkalut ovat jo kypsiä, koko mallintarkastusprosessin läpikäynti sisältää edelleen monia vaiheita, jotka joko vaativat asiantuntemusta, tai koostuvat yksinkertaisesta ja toistuvasta käsityöstä. Järjestelmästä on ensin laadittava malli, ja lisäksi järjestelmään kohdistuvat vaatimukset on formalisoitava mallintarkastimen (tietokoneohjelma, jolla mallintarkastusta tehdään) käyttämään muotoon. Jos jokin mallin suoritus on vaatimusten vastainen, mallintarkastin palauttaa astaesimerkin, joka kuvaa vaatimuksen rikkovan suorituspolun. Vastaesimerkkien tulkinta ilman tietoteknisiä apuvälineitä on työlästä. Käytännön sovelluksissa on havaittu, että toimilohkokaaviopohjaisten järjestelmäkuvausten mallintarkastusta voidaan huomattavasti helpottaa rakentamalla malli modulaarisesti, valmiin toimilohkokirjaston perusteella. Käynnissä onkin työkalukehitys, jonka tavoitteena on automatisoida useita mallintarkastuksen työvaiheita. NuSMV-mallintarkastin on tarkoitus liittää Simanticsiin, joka on avoimen lähdekoodin ohjelmistoalusta eri mallinnus- ja simulointityökalujen integrointiin. Simanticsin avulla malli voitaisiin paitsi laatia graafisen käyttöliittymän avulla, jopa luoda automaattisesti jostain muusta, esim. prosessisimulaattorille (kuten Apros) laaditusta automaatiojärjestelmän mallista. Vaikkei kaikkia työvaiheita saataisikaan helposti automatisoitua, tavoitteena on kuitenkin tuoda mallintarkastus lähemmäs automaatiojärjestelmän suunnitteluvaihetta