An Architecture for Verification with Extended Labeled Transition Systems
Kervinen, Oski (2015)
Kervinen, Oski
2015
Teknis-luonnontieteellinen koulutusohjelma
Luonnontieteiden tiedekunta - Faculty of Natural Sciences
This publication is copyrighted. You may download, display and print it for Your own personal use. Commercial use is prohibited.
Hyväksymispäivämäärä
2015-02-04
Julkaisun pysyvä osoite on
https://urn.fi/URN:NBN:fi:tty-201501291037
https://urn.fi/URN:NBN:fi:tty-201501291037
Tiivistelmä
This thesis lays out a common architecture for a software system meant for verification of correctness of concurrent state machines. The purpose of the architecture is to enable implementation and combination of different reductions and other manipulations, that give perspectives into the behaviour of the system.
The LTS model and associated techniques are presented for a mathematical basis for the system. The system is made flexible using extensive modularization. Even techniques traditionally contained inside the parallel composer, such as cut states and stubborn sets are extracted into modules. Techniques are presented to avoid the performance loss of modularization using compile time processing.
The LTS model and associated techniques are presented for a mathematical basis for the system. The system is made flexible using extensive modularization. Even techniques traditionally contained inside the parallel composer, such as cut states and stubborn sets are extracted into modules. Techniques are presented to avoid the performance loss of modularization using compile time processing.