Sign In

Mallintarkastus

Mallintarkastus

Mallintarkastus on tehokas järjestelmien verifiointiin soveltuva formaali menetelmä, jonka edut tulevat esille erityisesti silloin kun tutkittavan järjestelmän tila-avaruus kasvaa suureksi.

Hyvänä esimerkkinä toimii logiikkapiiri, jonka ulostulot määräytyvät vain ja ainoastaan sisäänmenojen perusteella. Kun sisäänmenojen määrä kasvaa kymmeniin, piiri on lähes mahdoton tarkastaa kattavasti manuaalisin keinoin tai simuloimalla. Alla olevassa taulukossa on esitetty kombinaatiopiirin sisääntulojen lukumäärän vaikutus piirin tila-avaruuden kokoon.


 

Inputtien määrä Tila-avaruus
2 4
8 256
30 ~10^9
100 ~10^30

 


 

Kun piiriin vielä lisätään ajastimia, viiveitä, muistielementtejä ja takaisinkytkentöjä, tila-avaruus kasvaa eksponentiaalisesti ja totutut verifiointimenetelmät eivät enää toimi. Mallintarkastuksessa tutkitaan toteuttaako järjestelmän malli sille asetetut vaatimukset. Tyypillisesti järjestelmästä tehdään tilakonemalli ja tarkastettava ehto ilmaistaan temporaalilogiikan lausekkeena. Mallin tilasiirtymät esitetään saavutettavuusgraafina, joka kuvaa mallin kaikki mahdolliset käyttäytymiset. Tarkastettavan ehdon päteminen tutkitaan siis kattavasti koko tila-avaruuden suhteen. Jos järjestelmässä on esimerkiksi 10 sisääntuloa, muutama viive, muutama aikapulssi ja yksi takaisinkytkentä, sen tila-avaruus kasvaa helposti yli 10^10. Tämän kokoisten järjestelmien mallintarkastusajat vaihtelevat tyypillisesti muutamista sekunneista muutamiin minuutteihin, tarkastettavasta ehdosta ja viiveiden skaalasta riippuen. Mallin luominen ja muuttaminen on suoraviivaista ja suhteellisen nopeaa. Kun malli on kerran tehty, sen avulla voidaan helposti tutkia miten suunnittelumuutokset vaikuttavat järjestelmän käyttäytymiseen ja pätevätkö vaadittavat ominaisuudet myös muutetussa mallissa.