Methodology of Dynamical Analysis of SDL Programs Using Predicate/Transition Nets
No Thumbnail Available
Journal Title
Journal ISSN
Volume Title
Helsinki University of Technology |
Diplomityö
Checking the digitized thesis and permission for publishing
Instructions for the author
Instructions for the author
Author
Date
1997
Department
Major/Subject
Digitaalitekniikka
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.Description
Supervisor
Ojala, LeoThesis advisor
Husberg, NisseKeywords
reachability analysis, SDL, SDL, PROD, formal methods, saavutettavuusanalyysi, Predicate/Transition nets, formaalit menetelmät, verification, predikaatti/transitio -verkot, PROD, verifiointi