Model Checking Software /
Systémy které navrhujeme jsou čím dál složitější a je často mimo lidské možnosti ověřit jejich korektnost. Výzkum v oblasti formálních metod vede k implementaci automatických nástrojů, které nám můžou s tímto úkolem pomoct. V současné době se však z různých důvodů užívá formálních metod pouze v ojed...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2015
|
| Témata: | |
| On-line přístup: | http://is.muni.cz/th/139761/fi_d/ |
| Shrnutí: | Systémy které navrhujeme jsou čím dál složitější a je často mimo lidské možnosti ověřit jejich korektnost. Výzkum v oblasti formálních metod vede k implementaci automatických nástrojů, které nám můžou s tímto úkolem pomoct. V současné době se však z různých důvodů užívá formálních metod pouze v ojedinělých případech. Obecným cílem této práce je zlepšit použitelnost metody ověřování modelu v návrhu a implementaci programů. Tato práce si klade za úkol přispět k dostupným znalostem v několika oblastech úzce spjatých s jejími cíly. V první řadě popisuje a implementuje interpret pro LLVM bitkód, který je centrální součástí nástroje pro ověřování programů. Poté uvede několik zlepšení tohoto základního interpretu: redkuce τ a τ+ pro zmenšení stavového prostoru vícevláknových programů, redukci pomocí symetrie haldy která činí dynamickou paměť praktickou a podporu výjimek nutnou pro verifikaci realistického kódu v jazyce C++. Za účelem zachycení složitého chování programů práce navrhuje nový j The systems we design are increasing in complexity and it is often beyond human capacity to verify their correctness. Research in formal methods has provided us with automated tools that can help ensure correctness of a system that is beyond our capabilities to check manually. Nowadays, for a variety of reasons, such tools are applied only to a very limited number of systems. The broad goal of this thesis is to improve applicability of model checking in design and implementation of general-purpose computer software. This thesis seeks to contribute to the state of the art in a number of areas closely aligned with this goal. Primarily, we describe and implement an interpreter for LLVM bitcode -- a centrepiece of a software model checker. We then introduce a number of improvements over the basic interpreter: τ and τ+ reduction to trim state spaces of threaded programs, heap symmetry reduction to make model checking with dynamic memory practical, exception handling which allows for verifi |
|---|---|
| Popis jednotky: | Vedoucí práce: Jiří Barnat |
| Fyzický popis: | 188 stran |