Detail produktu
Replay Tracer & BMC
Vznik: 2010
Fiedor Jan, Ing., Ph.D. (UITS FIT VUT)
Křena Bohuslav, Ing., Ph.D. (UITS FIT VUT)
Letko Zdeněk, Ing., Ph.D. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
prohledávací strategie, model checking, bounded model checking, Java, verifikace
Tento nástroj byl vyvinut za účelem verifikování Java programů s paralelismem. Byla navržena prohledávací strategie stavovým prostorem do podezřelého stavu resp. do jeho okolí a z toho stavu je možné provést bounded model checking. Prvním krokem je zaznamenaní jednoho běhu programu (pomocí nástroje IBM ConTest). Druhým krokem je přehrání zaznamenaného běhu v model checkeru Java PathFinder a následné provedení bounded model checkingu.
Výhodou tohoto přístupu je možnost začít verifikaci nejen pouze z dosaženého (podezřelého) stavu cesty, ale i z předcházejícího stavu, čímž dochází k lepšímu pokrytí okolí daného stavu.
FREEWARE LICENCE VUT V BRNĚ
Verze 1.
Copyright (c) 2010, Vysoké učení technické v Brně (VUT v Brně), Antonínská 548/1, PSČ 601 90
---------------------------------------------------------------------------------------------------------------------------------------------------
INSTALACÍ, KOPÍROVÁNÍM NEBO JINÝM POUŽITÍM SOFTWARE POTVRZUJETE, ŽE SOUHLASÍTE S PODMÍNKAMI TÉTO LICENČNÍ SMLOUVY. POKUD S TĚMITO PODMÍNKAMI NESOUHLASÍTE, SOFTWARE NEINSTALUJTE, NEKOPÍRUJTE ANI NEPOUŽÍVEJTE.
JESTLIŽE NEMÁTE PLATNOU LICENCI NA SOFTWARE, NEJSTE OPRÁVNĚNI SOFTWARE INSTALOVAT, KOPÍROVAT ANI JINAK POUŽÍVAT.
Definice:
Software se pro účely této smlouvy rozumí počítačový program (skupina počítačových programů tvořící jeden funkční celek) schopný autorskoprávní ochrany a s ním související dokumentace.
Každý, kdo použije Software, stává se Uživatelem. Uživatel se zavazuje dodržovat tyto licenční podmínky.
VUT V BRNĚ (DÁLE JEN JAKO POSKYTOVATEL) UDĚLUJE LICENCI K POUŽÍVÁNÍ SOFTWARE ZA NÁSLEDUJÍCÍCH PODMÍNEK:
-
Uživatel smí bezplatně užívat Software pro vlastní potřebu k nekomerčním účelům.
-
Uživatel smí kopírovat a šířit doslovné kopie spustitelného Software (udělovat sublicence) na libovolném médiu, za předpokladu, že na každé kopii viditelně a náležitě zveřejní zmínku o autorských právech, ponechá ne-dotčené všechny zmínky vztahující se k této licenci a dá každému příjemci spolu se Software kopii této licenční smlouvy.
-
Uživatel nesmí zasahovat do programového kódu Software, zejména nesmí zpětně analyzovat, dekompilovat nebo jinak upravovat Software, modifikovat anebo používat jeho části v jiném software a tak vytvořit dílo založené na Software, a kopírovat a rozšiřovat takové modifikace či dílo.
-
Uživatel nesmí užívat Software jiným způsobem než výslovně uvedeným v této licenci. Pokud má Uživatel zájem o jiné způsoby užívání Software, zejména využití ke komerčním účelům, může kontaktovat poskytovatele a dojednat podmínky úplatné licence zvláštní smlouvou. Jakýkoli jiný pokus o kopírování, modifikování, poskytnutí sublicence anebo šíření Software je neplatný a má za následek automatický zánik oprávnění z této licenční smlouvy.
-
VZHLEDEM K BEZPLATNÉMU POSKYTNUTÍ LICENCE K SOFTWARE SE NA SOFTWARE NEVZTAHUJE ŽÁDNÁ ZÁRUKA, A TO V MÍŘE POVOLENÉ ZÁKONEM. POKUD NENÍ PÍSEMNĚ STANOVENO JINAK, POSKYTUJÍ DRŽITELÉ AUTORSKÝCH PRÁV POPŘÍPADĚ JINÉ STRANY SOFTWARE "TAK, JAK JE", BEZ ZÁRUKY JAKÉHOKOLIV DRUHU, AŤ VÝSLOVNÉ NEBO KONKLUDENTNÍ, VČETNĚ, ALE NEJENOM, ZÁRUK ZA KVALITU A VÝKONNOST SOFTWARE, ZA PRODEJNOST A VHODNOST PRO URČITÝ ÚČEL.
POSKYTOVATEL V ŽÁDNÉM PŘÍPADĚ NEODPOVÍDÁ ZA ŠKODY, VČETNĚ VŠECH OBECNÝCH, SPECIÁLNÍCH, SKUTEČNÝCH ŠKOD NEBO UŠLÉHO ZISKU VYPLÝVAJÍCÍCH Z UŽÍVÁNÍ ANEBO NESCHOPNOSTI UŽÍVAT SOFTWARE (VČETNĚ ALE NIKOLI JEN, ZTRÁTY NEBO ZKRESLENÍ DAT, TRVALÝCH ŠKOD ZPŮSOBENÝCH UŽIVATELI NEBO TŘETÍM STRANÁM, SELHÁNÍ FUNKCE SOFTWARE V SOUČINNOSTI S JINÝMI SOFTWARE, NEBO V PŘÍPADĚ, ŽE PROGRAM PORUŠUJE PRÁVA TŘETÍCH OSOB), A TO I V PŘÍPADĚ, ŽE POSKYTOVATEL VĚDĚL O MOŽNOSTI TAKOVÝCH ŠKOD), TO VŠE V NEJŠIRŠÍ MOŽNÉ MÍŘE POVOLENÉ ZÁKONEM.
Závěrečná ustanovení:
Nevynutitelnost anebo neplatnost anebo neúčinnost kteréhokoli ujednání této smlouvy neovlivní vynutitelnost anebo platnost anebo účinnost jejích ostatních ustanovení.
Uživatel je povinen zabezpečit dodržování těchto licenčních podmínek případnou třetí osobou, která má přístup k jím užívané kopii Software.
Otázky touto smlouvou neupravené včetně otázek jejího vzniku a zániku se řídí českým právem. V případě soudní-ho sporu budou příslušné české obecné soudy.
Instalací, kopírováním nebo jiným použitím Software Uživatel prohlašuje, že se s obsahem této smlouvy důkladně seznámil, že je souhlas s touto smlouvou projevem jeho skutečné, vážné, svobodné a určité vůle prosté omylu a že není uzavřena v tísni za nápadně nevýhodných podmínek.
Bohatý modelovací jazyk -- infrastruktura pro spolehlivé počítačové systémy (IC0901)
Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů (GD102/09/H042)
Práce se složitými datovými strukturami a paralelismem v prostředí Rich Model Toolkit (OC10009)
SHADOWS - A Self-Healing Approach to Designing Complex Software Systems ()
Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti (GAP103/10/0306)
Výzkum informačních technologií z hlediska bezpečnosti (MSM0021630528)