| Název: | Návrh spolehlivých systémů s využitím formálních metod |
| Další názvy: | Design of Reliable Systems Using Formal Methods |
| Autoři: | Cipov, Peter |
| Vedoucí práce/školitel: | Rohlík, Ondřej |
| Oponent: | Brada, Přemysl |
| Datum vydání: | 2012 |
| Nakladatel: | Západočeská univerzita v Plzni |
| Typ dokumentu: | diplomová práce |
| URI: | http://hdl.handle.net/11025/3063 |
| Klíčová slova: | formální metody;CORDET;spolehlivé systémy;Java PathFinder;lineární temporální logika |
| Klíčová slova v dalším jazyce: | formal methods;Java PathFinder;SPIN;model checking;linear temporal logic;CORDET;reliable systems |
| Abstrakt: | Formálne metódy sú skúmané už niekoľko desaťročí a stali sa z nich veľmi mocné nástroje. Existujú v rôznych variantách od čisto teoretických, k skoro automatickým. Ale aj tak, kontrola formalych vlastností nie je denným chlebom každého programátora. V priemysle sú formálne metódy použité iba pre veľmi drahé, spoľahlivé systémy, kde sú iba niektoré časti programu, jednotlivé algoritmy alebo protokoly transformované na model, ktorý je následne preverený. Táto práca používa spôsob formálnej verifikácie, ktory má za cieľ overevovať omnoho väčšie celky ako jednolitvé algoritmy. Práca je zameraná na využitie takýchto meótod za účelom kontroly výstupov z CORDET projektu, ktorý je zameraný na vývoj palubných satelitných systémov. Práca skúma a predvádza aktuálne možnosti takejto kontroly. |
| Abstrakt v dalším jazyce: | The formal methods have been researched over several decades and they became very powerful tools. There are varieties of approaches from purely theoretical to solutions that are nearly automatic. Even so, formal checker is not daily bread of every software developer. In the industry formal checkers are used only for very expensive, mission critical software where only a few program parts, separate algorithms or protocols are transformed to model which is under check. This thesis tries to use other promising way of formal verification that aims to be used on much bigger units than a single algorithm. This thesis is focused on using such checker for purposes of CORDET project which is oriented on development of onboard satellite systems. It examines and demonstrates current checker characteristics. |
| Práva: | Plný text práce je přístupný bez omezení. |
| Vyskytuje se v kolekcích: | Diplomové práce / Theses (KIV) |
Soubory připojené k záznamu:
| Soubor | Popis | Velikost | Formát | |
|---|---|---|---|---|
| thesis.pdf | Plný text práce | 10,4 MB | Adobe PDF | Zobrazit/otevřít |
| A09N0173Pposudek-ved.pdf | Posudek vedoucího práce | 383,92 kB | Adobe PDF | Zobrazit/otevřít |
| A09N0173Pposudek-op.pdf | Posudek oponenta práce | 612,3 kB | Adobe PDF | Zobrazit/otevřít |
| A09N0173Pobhajoba.pdf | Průběh obhajoby práce | 170,9 kB | Adobe PDF | Zobrazit/otevřít |
Použijte tento identifikátor k citaci nebo jako odkaz na tento záznam:
http://hdl.handle.net/11025/3063Všechny záznamy v DSpace jsou chráněny autorskými právy, všechna práva vyhrazena.