Maria

Modulaarinen saavutettavuusanalysaattori

Maria on rinnakkaisten järjestelmien saavutettavuusanalysaattori, joka perustuu algebrallisiin järjestelmäverkkoihin, jotka ovat korkean tason Petri-verkkoja. Se on kirjoitettu C++:lla, ja se on vapaasti hyödynnettävissä GNU General Public Licensen ehdoilla.

Julkaistut versiot

0.1 17. syyskuuta 1999
0.2 10. elokuuta 2001
1.0 1. marraskuuta 2001
1.0.1 5. helmikuuta 2002
1.1 23. huhtikuuta 2002
1.2 23. kesäkuuta 2002
1.3 4. syyskuuta 2002
1.3.1 15. marraskuuta 2002
1.3.2 5. joulukuuta 2002
1.3.3 9. joulukuuta 2002
1.3.4 20. kesäkuuta 2003
1.3.5 29. heinäkuuta 2005

Laajennuksia

Maria-työkaluun on erikseen saatavilla LTL-X-mallintarkistin modulaarisille tila-avaruuksille. Koska toteutus on puutteellinen, se jaetaan erillisinä muutoksina versiolle 1.3.4 ja muutoksina versiolle 1.3.5. Lue lisätietoja ja asennusohjeet.

Esittelyaineistoa

Lue myös hankkeen taustasta ja tutustu julkaisuihimme.

Työkalun tila

Saavutettavuusanalysaattori, lennosta toimiva mallintarkistin ja graafityökalu ovat olleet toiminnassa vuodesta 1999, jolloin julkaistiin versio 0.1. Vuonna 2001 julkaistuissa versioissa 0.2 ja 1.0 on kehittyneempiä toimintoja kuten reiluusoletuksia hyödyntävä mallintarkistin, käännökset matalan tason verkoksi ja C-koodiksi sekä graafinen käyttöliittymä.

Saavutettavuusgraafin esitystyökalu perustuu GraphViz-ohjelmistoon, jonka AT&T on kehittänyt graafien esittämistä varten. Työkalusta on kaksi toteutusta:

Marko Mäkelä lopetti työkalun kehittämisen vuonna 2004. Versio 1.3.5 (jossa on vähäisiä siirrettävyyden ja tehokkuuden parannuksia) jäänee viimeiseksi hänen julkaisemakseen.

Ulkoiset työkalut

Ohjelman saatavuus

Ohjelmiston lähdekoodin jakelupaikka on http://www.tcs.hut.fi/Software/maria/src/. Ajettavaksi ohjelmaksi sen voi kääntää esimerkiksi GCC:llä.

Voit myös kokeilla uusinta kehitteillä olevaa lähdekoodia ja käyttöohjetta.

Windows-käyttäjien iloksi tarjoamme zip-pakkauksen mingw:n ristiinkääntäjäksi asennetulla gcc-2.95.2:lla käännetystä ajettavasta ohjelmasta. Tämä versio on alkutekijöissään: C-koodin tuottaminen ei toimi eikä graafien esittäminen kuvina onnistu.

Dokumentaatio

Maria 1.3.4:n käyttöohje, joka on tuotettu GNU-hankkeen Texinfo-järjestelmällä, on saatavissa PDF-muodossa.

Marian saavutettavuusgraafitiedostojen rakenne ja tilakoneiden kielet on kuvattu erikseen.

Marian ohjelmointityyli perustuu Ellemtelin suosituksiin.


Tämä sivu on saatavissa myös seuraavilla kielillä:
English
Oletuskielen asettamisohjeet


Marko Mäkelä, Maria-hanke

Valid HTML 4.01!