|
|
Analyzer of Windows Kernel Models
Calta, Jan ; Ježek, Pavel (vedoucí práce) ; Šerý, Ondřej (oponent)
Diplomová práce předkládá nástroj pro analýzu modelů ve specifikačním jazyce DeSpec a pro jejich překlad do modelovacího jazyka Zing. Výsledné modely pak mohou být verifikovány model checkerem Zing. Jazyk DeSpec je navržen především pro specifikaci prostředí, ve kterém pracují ovladače operačních systémů rodiny Windows NT. Umožňuje abstrahovat toto prostředí objektově orientovaným způsobem a používá formule lineární temporální logiky k popisu pravidel, jejichž splnění jádro OS Windows od ovladačů vyžaduje. Jazyk Zing je navržen pro popis vykonavatelných modelů software včetně paralelismu, které mohou být dale zkoumány model checkerem Zing. Vlastnosti k ověření jsou vyjádřeny příkazy assert. Dosud neexistoval způsob, jak automaticky extrahovat ze specifikace v DeSpecu model, který by mohl být formálně verifikován model checkerem. Překladač z DeSpecu do Zingu hraje v tomto úkolu zásadní roli. Práce ukazuje, že je možné překládat specifikace v DeSpecu do modelů v Zingu a tedy že DeSpec je vhodným jazykem pro model checking cílového prostředí. Uvedený nástroj umožňuje kontrolu správnosti specifikace v DeSpecu a za omezení daných absencí dalších nezbytných nástrojů umožňuje překlad vybrané podmnožiny specifikací do Zingu.
|
|
|
Institucionalizace oboru stranických dějin a dějin dělnického hnutí na Filosofické fakultě UK. v letech 1953-1970
Calta, Jan ; Rákosník, Jakub (vedoucí práce) ; Sommer, Vítězslav (oponent)
(česky) Práce se zabývá tématem utváření stranické historiografie v padesátých a šedesátých letech dvacátého století. Zkoumá tuto problematiku ve dvou rovinách. První rovinou je institucionalizace stranické historiografie na filozofické fakultě Univerzity Karlovy. Zmapován je vznik, vývoj a zánik katedry dějin KSČ (dějin dělnického hnutí) se zaměřením na klíčové mezníky v letech 1953 (založení katedry), 1958 (restrikce pedagogického stavu), 1964 (reorganizace, sloučení a vznik katedry dějin dělnického hnutí) a 1970 (zrušení katedry). Dále je věnována pozornost personálnímu obsazení a snaze vytvořit typologický profil členů katedry, kteří patřili k nastupující generaci stranických historiků. Druhou rovinou bádání je podíl stranických historiků z katedry dějin KSČ (dějin dělnického hnutí) na utváření a formulaci nových historických narativů, které poskytovaly legitimizační rámec komunistickému projektu přeměny společnosti. Zkoumány jsou možnosti a meze stranické historiografie v dobovém politickém a sociálním kontextu a také možnosti jejího metodologického uchopení. Vývoj stranické historiografie je členěn do třech fází - fáze stalinského diskurzu, fáze poststalinského diskurzu a fáze reformního diskurzu. Powered by TCPDF (www.tcpdf.org)
|
|
|
Postoj F. D. Roosevelta k otevření druhé fronty
Calta, Jan ; Stellner, František (vedoucí práce) ; Koura, Jan (oponent)
Tato práce se zabývá problematikou britsko - amerického spojenectví v průběhu Druhé světové války a snahou spojenců provést masivní invazi v západní Evropě. Vše je nahlíženo především z perspektivy amerického prezidenta Roosevelta. V první části je analyzováno období americké neutrality před útokem na Pearl Harbor a snaha prezidenta Roosevelta připravit americkou společnost na vstup do války. Druhá část popisuje období od vstupu Spojených států do války do první spojenecké invaze v severní Africe. Pozornost je věnována především spojeneckým konferencím, kde se utvářela hlavní vojenská strategie. Zohledněn je také vliv amerického veřejného mínění na postoj prezidenta Roosevelta. Závěrečná část se zabývá obdobím od invaze v severní Africe po definitivní rozhodnutí o otevření druhé fronty na konferenci v Teheránu v prosinci 1943. V tomto období se již začala postupně projevovat převaha Spojených států v utváření spojenecké strategie.
|
|
|
Analyzer of Windows Kernel Models
Calta, Jan ; Šerý, Ondřej (oponent) ; Ježek, Pavel (vedoucí práce)
Diplomová práce předkládá nástroj pro analýzu modelů ve specifikačním jazyce DeSpec a pro jejich překlad do modelovacího jazyka Zing. Výsledné modely pak mohou být verifikovány model checkerem Zing. Jazyk DeSpec je navržen především pro specifikaci prostředí, ve kterém pracují ovladače operačních systémů rodiny Windows NT. Umožňuje abstrahovat toto prostředí objektově orientovaným způsobem a používá formule lineární temporální logiky k popisu pravidel, jejichž splnění jádro OS Windows od ovladačů vyžaduje. Jazyk Zing je navržen pro popis vykonavatelných modelů software včetně paralelismu, které mohou být dale zkoumány model checkerem Zing. Vlastnosti k ověření jsou vyjádřeny příkazy assert. Dosud neexistoval způsob, jak automaticky extrahovat ze specifikace v DeSpecu model, který by mohl být formálně verifikován model checkerem. Překladač z DeSpecu do Zingu hraje v tomto úkolu zásadní roli. Práce ukazuje, že je možné překládat specifikace v DeSpecu do modelů v Zingu a tedy že DeSpec je vhodným jazykem pro model checking cílového prostředí. Uvedený nástroj umožňuje kontrolu správnosti specifikace v DeSpecu a za omezení daných absencí dalších nezbytných nástrojů umožňuje překlad vybrané podmnožiny specifikací do Zingu.
|
host ::
RSS.