Methodology of Dynamical Analysis of SDL Programs Using Predicate/Transition Nets

Thumbnail Image

URL

Journal Title

Journal ISSN

Volume Title

Helsinki University of Technology | Diplomityö
Checking the digitized thesis and permission for publishing
Instructions for the author

Authors

Date

1997

Department

Tietotekniikan osasto

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, Leo

Thesis advisor

Husberg, Nisse

Keywords

reachability analysis, SDL, SDL, PROD, formal methods, saavutettavuusanalyysi, Predicate/Transition nets, formaalit menetelmät, verification, predikaatti/transitio -verkot, PROD, verifiointi

Other note

Citation

Permanent link to this item

https://urn.fi/URN:NBN:fi:aalto-2020120343921

Collections

[dipl] Teknillinen korkeakoulu / TKK