search query: @keyword verifiointi / total: 19
reference: 16 / 19
Author: | Malmqvist, Markus |
Title: | Methodology of Dynamical Analysis of SDL Programs Using Predicate/Transition Nets |
Predikaatti/Transitio -verkkojen avulla tapahtuvan SDL-ohjelmien dynaamisen analysoinnin metodologia | |
Publication type: | Master's thesis |
Publication year: | 1997 |
Pages: | iv + 76 Language: eng |
Department/School: | Tietotekniikan osasto |
Main subject: | Digitaalitekniikka (Tik-79) |
Supervisor: | Ojala, Leo |
Instructor: | Husberg, Nisse |
OEVS: | Electronic archive copy is available via Aalto Thesis Database.
Instructions Reading digital theses in the closed network of the Aalto University Harald Herlin Learning CentreIn the closed network of Learning Centre you can read digital and digitized theses not available in the open network. The Learning Centre contact details and opening hours: https://learningcentre.aalto.fi/en/harald-herlin-learning-centre/ You can read theses on the Learning Centre customer computers, which are available on all floors.
Logging on to the customer computers
Opening a thesis
Reading the thesis
Printing the thesis
|
Location: | P1 Ark T80 | Archive |
Keywords: | reachability analysis SDL formal methods Predicate/Transition nets verification PROD SDL PROD saavutettavuusanalyysi formaalit menetelmät predikaatti/transitio -verkot verifiointi |
Abstract (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 record number: 12285
+ add basket
INSSI