|
|
Distributed Behavior Protocol Checker
Poch, Tomáš ; Adámek, Jiří (oponent) ; Kofroň, Jan (vedoucí práce)
Nárůst dostupné výpořetní síly umožnil v posledních letech praktické využití formální verifikace softwarových systémů. Nejpalčivějším problémem, který zabraňuje širšímu využití však zůstává velikost stavových prostorů. Proto jsou tyto techniky zatím omezeny na relativně malé úlohy. Jednou z možností jak podstatně snížit počet stavů je modelování softwaru pomocí behavior protokolů. [1] Jedná se o regulární výrazy, které popisují chování softwarových komponent. Konkrétní implementace komponenty je tedy ověřena jen jednou oproti protokolu a při verifikaci celé aplikace je již skryta. Ta se pak redukuje na ověření toho, že protokoly komponent ze kterých se aplikace skládá k sobě pasují. Nicméně velikost i takto zjednodušeného stavového prostoru bývá typicky exponenciální vzhledem k délce popisu modelu. Distribuovaný průchod stavovým prostorem společně s jeho generováním 'za letu' [2] by měl ještě více rozšířit rozsah problémů zvládnutelných touto technikou.
|
|
|
Extending Java PathFinder with Behavior Protocols
Plšek, Aleš ; Kofroň, Jan (oponent) ; Adámek, Jiří (vedoucí práce)
Komponentově orientované programování, vyuřívající behavior protokoly pro specifikaci chovaní komponent, představuje efektivní přístup k vývoji softwarových aplikací. Jedním z prostředků jak ještě více usnadnit vývoj je i analýza korektnosti systému. Avšak bez ověření, že implementace komponent dodržují dané behavior protokoly, nemůže být analýza korektnosti systému formálně považována za úplnou. Tato práce předkládá způsob jak ověřit, zda je implementace komponenty v souladu s daným behavior protokolem. Navržené řešení využívá nástroj Java PathFinder Model Checker k ověření implementace komponenty a tímto ambiciózním způsobem úspěšně čelí jednomu z otevřených problémů při vývoji komponentových aplikací.
|
|
|
Slévání rozdílných verzí textových souborů
Trochtová, Lenka ; Kofroň, Jan (oponent) ; Ježek, Pavel (vedoucí práce)
Cílem této práce bylo vytvořit program Merge sloužící k porovnávání a slévání dvou nebo tří verzí textových souboru a adresářů. Práce se zabývá programem Merge jak z uživatelského, tak i z programátorského hlediska. Součástí práce je uvedení do problematiky porovnávání a slévání souborů, porovnání programu Merge s některými existujícími nástroji, stručný popis základních funkcí programu, popis návrhu a implementace programu včetně použitých algoritmů textového a adresářového porovnání.
|
|
|
Combining temporal logic and behavior protocols
Mandys, Petr ; Kofroň, Jan (oponent) ; Adámek, Jiří (vedoucí práce)
V této diplomové práci se zabýváme jednou ze slabin temporální logiky - obtížnou čitelností temporálních formulí popisujících komplexní vlastnosti. Představíme novou temporální logiku "BP-CTL", která vychází z Computational Tree Logic (CTL) a rozšiřuje ji o operátory zčásti převzaté z behaviorálních protokol (BP) a zčásti nově definované. Text práce je rozdělen do několika částí. Nejprve seznámíme čtenáře s širším kontextem problému, kterým se zabýváme. Dále popíšeme nové operátory a ukážeme jejich použítí na malých příkladech. Poté formálně zadefinujeme výsledný jazyk (BP-CTL). V další části dokážeme použitelnost BP-CTL v praxi a představíme nástroj, nazvaný bpctl, pro ověřování vlastností zapsaných pomocí BP-CTL. Na závěr zhodnotíme a shrneme naši práci. Text je dále doplněn o dodatky obsahující detailní popis použitých formalizmů, mapovací tabulky paternů shromážděných v rámci projektu Property Specification Patterns pro BP-CTL a uživatelský manuál bpctl.
|
|
|
Post-quantum alternative to secure sockets
Behún, Marek ; Kratochvíl, Miroslav (vedoucí práce) ; Kofroň, Jan (oponent)
Cílem této práce je implementovat softwarovou knihovnu, která umožní šifrovat interaktivní síťovou komunikaci pomocí kryptografického protokolu podobného SSL nebo TLS, jehož bezpečnost není ohrožena útočníkem vlastnícím kvantový počítač. Pro dosážení dané úrovně bezpečnosti výsledný software používá algoritmus na výměnu klíčů zvaný Supersingular Isogeny Diffie Hellman (SIDH). Software je poměrně jednoduchý, přenosný a nezávislý na specifikách konkrétního operačního systému. Práce také podává zhuštěný úvod do teorie, na které je algoritmus SIDH postaven, psaný pro cílovou skupinu studentů bakalářských a magisterských kurzů informatiky. Powered by TCPDF (www.tcpdf.org)
|
|
|
Ověřování asercí kódu pomocí zpětné symbolické exekuce
Husák, Robert ; Kofroň, Jan (vedoucí práce) ; Parízek, Pavel (oponent)
Pro prevenci, odhalování a opravování chyb v softwaru existuje celá řada nástrojů pro programátory, přičemž některé z nich umožňují pracovat přímo se sémantikou programu. V případě jazyka C# jsou hlavními zástupci Microsoft FxCop, Code Contracts a Pex. Použití těchto nástrojů může velkou měrou přispět k vysoké spolehlivosti programů. Jejich úplné zapojení do procesu vývoje software ve firmách je bohužel značně náročné na prostředky. Z tohoto důvodu jsme vytvořili AskTheCode, zjednodušený nástroj pro verifikaci asercí kódu. Jeho hlavním účelem je pomoci uživateli s jedním konkrétním problémem, který v daném okamžiku řeší. Vzhledem k tomuto přístupu jsme jej implementovali pomocí zpětné symbolické exekuce. Přestože je momentálně schopen pracovat pouze se základními konstrukty a typy jazyka C#, srovnání s existujícími nástroji ukázalo, že při dalším rozvoji má potenciál poskytnout uživateli významnou přidanou hodnotu. Powered by TCPDF (www.tcpdf.org)
|
|
|
Model checking softwarových komponent: úprava Java PathFinder pro spolupráci s Behavior Protocol Checker
Pařízek, P. ; Plášil, František ; Kofroň, Jan
Přestože existuje několik model checkerů pro software, které ověřují kód proti specifikaci zapsané např. v temporální logice a tzv. assertions, nebo ověřují nízkoúrovňové vlastnosti (jako neošetřené výjimky), žádný z nich nepodporuje ověřování softwarových komponent proti vyšší specifikaci chování. Tato zpráva popisuje náš přístup k model checkingu softwarových komponent implementovaných v jazyce Java proti specifikaci jejich chování definované pomocí protokolů chování, který využívá model checker Java PathFinder a protocol checker. Vlastnosti ověřované nástrojem Java PathFinder (korektnost sekvencí volání metod) se validují pomocí spolupráci s nástrojem protocol checker. Ukazujeme, že pouze návrhový vzor publisher/listener, označovaný za klíčový pro podporu rozšiřitelnosti v nástroji Java PathFinder, nebyl dostatečný pro tento typ ověřování (přestože byl pro nás velmi užitečný).
|
|
|
Rozšíření Behavior Protocols o data a multisynchronizaci
Kofroň, Jan
Použití Behavior Protocols pro specifikaci chování komponent v hierarchických komponentových modelech (SOFA, Fractal) se ukázalo být vhodným přístupem, pokud nás zajímá absence komunikačních chyb mezi komponentami v dané aplikaci. Během specifikace Fractalové komponentové aplikace zaměřené na kontrolu přístupu k internetu na letištích umožňující několik způsobů úhrady se projevilo několik nedostatků Behavior Protocols jako specifikační platformy. Dvě nejdůležitější zahrnují (i) nedostatečná vyjadřovací síla Behavior Protocols při specifikaci některých běžných vzorů chování a (ii) nedostatečný výkon aplikace Behavior Protocol Checker – nástroje použitého pro hledání kompozičních chyb mezi komunikujícími komponentami. Tento článek se soustředí na řešení prvního problému pomocí rozšíření formalismu Behavior Protocols.
|
|
|
Ověřování softwarových komponent: O překladu Behavior Protocols do Promely
Kofroň, Jan
Používání softwarových komponent patří k moderním přístupům k vytváření rozšiřitelných a spolehlivých aplikací. K zajištění vysoké spolehlivost by komponentová aplikace měla být verifikována, např. podstoupit model checking. Implementace aplikace je většinou příliš složitá, než aby mohla být verifikována na formální úrovni. Proto se používá model, který je abstrakcí této implementace. Behavior Protocols jsou platformou pro modelování chování softwarových komponent. V tomto článku navrhujeme metodu pro překlad specifikace Behavior Protocols do Promely, která je následně použita jako vstup pro model checker Spin. Pokud máme model v jazyku Promela popisující chování komponent, můžeme efektivně ověřovat kompatibilitu i LTL vlastnosti kooperujících komponent.
|
|
| |
host ::
RSS.