aalto1 untyped-item.component.html
Methodology of Dynamical Analysis of SDL Programs Using Predicate/Transition Nets
Loading...
URL
Journal Title
Journal ISSN
Volume Title
Helsinki University of Technology |
Master's thesis
Electronic archive copy is available via Aalto Thesis Database.
Checking the digitized thesis and permission for publishing
Instructions for the author
Instructions for the author
Location:
Authors
Date
Department
Major/Subject
Mcode
Tik-79
Degree programme
Language
en
Pages
iv + 76
Series
Abstract
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.