haku: @keyword predicate/transition nets / yhteensä: 6
viite: 2 / 6
Tekijä: | Malmqvist, Markus |
Työn nimi: | Methodology of Dynamical Analysis of SDL Programs Using Predicate/Transition Nets |
Predikaatti/Transitio -verkkojen avulla tapahtuvan SDL-ohjelmien dynaamisen analysoinnin metodologia | |
Julkaisutyyppi: | Diplomityö |
Julkaisuvuosi: | 1997 |
Sivut: | iv + 76 Kieli: eng |
Koulu/Laitos/Osasto: | Tietotekniikan osasto |
Oppiaine: | Digitaalitekniikka (Tik-79) |
Valvoja: | Ojala, Leo |
Ohjaaja: | Husberg, Nisse |
OEVS: | Sähköinen arkistokappale on luettavissa Aalto Thesis Databasen kautta.
Ohje Digitaalisten opinnäytteiden lukeminen Aalto-yliopiston Harald Herlin -oppimiskeskuksen suljetussa verkossaOppimiskeskuksen suljetussa verkossa voi lukea sellaisia digitaalisia ja digitoituja opinnäytteitä, joille ei ole saatu julkaisulupaa avoimessa verkossa. Oppimiskeskuksen yhteystiedot ja aukioloajat: https://learningcentre.aalto.fi/fi/harald-herlin-oppimiskeskus/ Opinnäytteitä voi lukea Oppimiskeskuksen asiakaskoneilla, joita löytyy kaikista kerroksista.
Kirjautuminen asiakaskoneille
Opinnäytteen avaaminen
Opinnäytteen lukeminen
Opinnäytteen tulostus
|
Sijainti: | P1 Ark T80 | Arkisto |
Avainsanat: | reachability analysis SDL formal methods Predicate/Transition nets verification PROD SDL PROD saavutettavuusanalyysi formaalit menetelmät predikaatti/transitio -verkot verifiointi |
Tiivistelmä (fin): | Rinnakkaisten ja hajautettujen järjestelmien voimakas yleistyminen on luonut uusia järjestelmien oikeellisuutta koskevia ongelmia. Tässä työssä esitellään automaattinen verifiointityökalu EMMA, joka käyttää predikaatti/transitio -verkkoja TNSDL-ohjelmien mallitukseen. Verifiointi perustuu PROD-analysaattorin avulla tapahtuvaan saavutettavuusanalyysiin. Monia tilaräjähdyksen välttämiseen tähtääviä menetelmiä mainitaan, kuten mallin optimointi, edistyneet tila-avaruuden generointialgoritmit ja suora TNSDL-ohjelmien muuntelu. Tässä työssä pääpaino on mallin optimoinnilla teollisia TNSDL-ohjelmia varten. Myös TNSDL-ohjelmien mallituksen pääperiaatteet selitetään. EMMA-projektissa on mallitettu koko TNSDL-kieli. Ero mallin ja implementaation välillä on pieni, koska molemmat on saatu automaattisesti samasta TNSDL-spesifikaatiosta. Saavutettavuusanalyysin tulokset muunnetaan takaisin TNSDL-kielelle, mikä tekee työkalun käytön helpommaksi verkkoteoriaan perehtymättömille. |
ED: | 1997-06-19 |
INSSI tietueen numero: 12285
+ lisää koriin
INSSI