aalto1 untyped-item.component.html
Reachability-based verification of DSS1 protocol
Loading...
URL
Journal Title
Journal ISSN
Volume Title
Helsinki University of Technology |
Master's thesis
Location:
Unless otherwise stated, all rights belong to the author. You may download, display and print this publication for Your own personal use. Commercial use is prohibited.
Authors
Date
Department
Major/Subject
Mcode
Tik-79
Degree programme
Language
en
Pages
71
Series
Abstract
Tutkimus rinnakkaisten ja hajautettujen järjestelmien alalla on tuottanut useita formalismeja, joita voidaan käyttää suurien järjestelmien verifioinnissa.
Tässä työssä esitetään DSS1 protokollan Petri verkkojen käyttöön perustuva mallitus ja analyysi.
Työssä on kehitetty käytännön menetelmiä signalointikanavien, ajastimien, siirtovirheiden ja ylemmän protokollakerroksen primitiivien mallintamiseen Petri verkkojen avulla.
Työssä on erityisesti keskitytty staattisten prioriteettien hyväksikäyttöön saavutettavuusgraafin generoinnin helpottamiseksi.
Protokollan määrityksestä löytyi kolme virhettä, jotka esitetään korjauksineen työn lopussa.