haku: @keyword saavutettavuusanalyysi / yhteensä: 13
hakutulos-lista
viite: 9 / 13
« edellinen | seuraava »
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
sulje

Digitaalisten opinnäytteiden lukeminen Aalto-yliopiston Harald Herlin -oppimiskeskuksen suljetussa verkossa

Oppimiskeskuksen 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

  • Aalto-yliopistolaiset kirjautuvat asiakaskoneille Aalto-tunnuksella ja salasanalla.
  • Muut asiakkaat kirjautuvat asiakaskoneille yhteistunnuksilla.

Opinnäytteen avaaminen

  • Asiakaskoneiden työpöydältä löytyy kuvake:

    Aalto Thesis Database

  • Kuvaketta klikkaamalla pääset hakemaan ja avaamaan etsimäsi opinnäytteen Aaltodoc-tietokannasta. Opinnäytetiedosto löytyy klikkaamalla viitetietojen OEV- tai OEVS-kentän linkkiä.

Opinnäytteen lukeminen

  • Opinnäytettä voi lukea asiakaskoneen ruudulta tai sen voi tulostaa paperille.
  • Opinnäytetiedostoa ei voi tallentaa muistitikulle tai lähettää sähköpostilla.
  • Opinnäytetiedoston sisältöä ei voi kopioida.
  • Opinnäytetiedostoa ei voi muokata.

Opinnäytteen tulostus

  • Opinnäytteen voi tulostaa itselleen henkilökohtaiseen opiskelu- ja tutkimuskäyttöön.
  • Aalto-yliopiston opiskelijat ja henkilökunta voivat tulostaa mustavalkotulosteita Oppimiskeskuksen SecurePrint-laitteille, kun tietokoneelle kirjaudutaan omilla Aalto-tunnuksilla. Väritulostus on mahdollista asiakaspalvelupisteen tulostimelle u90203-psc3. Väritulostaminen on maksullista Aalto-yliopiston opiskelijoille ja henkilökunnalle.
  • Ulkopuoliset asiakkaat voivat tulostaa mustavalko- ja väritulosteita Oppimiskeskuksen asiakaspalvelupisteen tulostimelle u90203-psc3. Tulostaminen on maksullista.
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
« edellinen | seuraava »
INSSI