Maria on Teknillisen korkeakoulun Tietojenkäsittelyteorian laboratorion nelivuotinen soveltava tutkimushanke, jonka eräs tavoite on formaalien menetelmien sovittaminen ohjelmistoteollisuuden tarpeisiin.
Hankkeen päätuote on rinnakkaisten järjestelmien mallien tutkimiseen sopiva ohjelmisto, jossa on saavutettavuusanalyysi sekä mallintarkistin turvallisuus- ja elävyysominaisuuksille. Mallit voi tehdä joko käsin tai koneellisesti muista kuvauskielistä kuten CCITT Specification and Description Language (SDL).
Hankkeen tärkeimpiä tavoitteita on pystyä analysoimaan SDL-kielellä kuvattuja telekommunikaatioprotokollia. SDL on kyettävä kääntämään tehokkaaksi mutta tarkaksi malliksi, ja tutkittavat ominaisuudet on kuvattava insinööreille riittävän helppotajuisella kielellä. Lopuksi analyysissä löytyneet vastaesimerkit on käännettävä alkuperäisen kuvauksen suorituspoluiksi ja tiloiksi.
SDL-kuvausten kääntäminen Petri-verkkomalleiksi ei ole uusi ajatus. Toteutuksia on SDL:n kaltaisille kielille (Emma TNSDL:lle) ja SDL:n osajoukoille. Emma-hankkeessa opittiin, että saavutettavuusanalysaattorissa on oltava monipuoliset tietotyypit, jotta SDL:n kaltaisesta korkean tason kielestä tehdystä käännöksestä tulisi tehokas, lyhyt ja luettava.
Eri Petri-verkkoluokille on monia analyysityökaluja, mutta mielestämme Maria-hankkeen työkalussa on ennen näkemättömän joustava tietotyyppijärjestelmä ja ilmaisuvoimaiset lausekkeet.