|
|
Analyzer of Windows Kernel Models
Calta, Jan ; Ježek, Pavel (advisor) ; Šerý, Ondřej (referee)
The thesis introduces a tool for analyzing models written in the specification language DeSpec and translating them into the Zing modeling language. Resulting models can be verified by the Zing model checker. The DeSpec language is designed primarily to specify the Windows NT kernel driver environment. It makes it possible to abstract this environment in the object-oriented way and it uses temporal logic patterns to capture rules imposed by the Windows kernel on drivers. The Zing language is designed to describe executable concurrent models of software, which can be explored by the Zing model checker. Properties to check are expressed by the assertions. So far, there has been no way to automatically extract a model from DeSpec specification and verify its properties by a model checker. The DeSpec-to-Zing compiler takes a crucial part in this task. The thesis demonstrates that it is feasible to translate DeSpec specifications into Zing models and that DeSpec is a suitable language for model checking of the Windows kernel driver environment. The introduced analyzer is capable to check correctness of DeSpec specifications and under the constrained conditions given by absence of other necessary tools it is capable to translate a subset of specifications into the Zing model.
|
|
|
Historiography of the Communist Party and the Working Class Movement and its Institutionalisation at the Faculty of Arts - Charles University in years 1953-1970
Calta, Jan ; Rákosník, Jakub (advisor) ; Sommer, Vítězslav (referee)
(in English): This work deals with the formation of party historiography in fifties and sixties of the twentieth century. It examines this issue in two ways. The first level is the institutionalization of party historiography at Faculty of Arts of Charles University. Establishment, development and abolition of the department of the History of the Communist party (History of Working class movement) is explored with focusing on key turning points in 1953 (establishment of the department), 1958 (restriction of teaching staff), 1964 (reorganization, merger and establishment of the department of the History of Working class movement) and 1970 (abolition of the department). Teaching staff is examined and attention is paid to the efforts to create typological profile of chair historians, who were part of emerging generation of party historians. The second level of the research is the participation of party historians in shaping and formulating new historical narratives, that provided legitimazing framework of communist project to social transformation. Attention is paid to possibilities and limits of party historiography in social and political context and its methodological base is also examined. The development of party historiography is divided into three phases - the phase of stalinist discourse, the...
|
|
|
F. D. Roosevelt's attitude towards opening the second front
Calta, Jan ; Stellner, František (advisor) ; Koura, Jan (referee)
The core of this work is aimed on the British - American alliance during the Second world war and the effort of allies carry out the massive cross - channel invasion. All this matters are reflected from the view of american president Roosevelt. In the first part is analyzed non - belligerent period of american neutrality before the attack at Pearl Harbor and the Roosevelt's effort prepare the american society for the entry to the war. The second part described the period from the american entry to the war until the first invasion in North Africa. The attention is aimed first of all on the diplomatic talks, where the Grand strategy was created. The influence of american public opinion on the Roosevelt's attitude is also reflected. The last part deals in the period from the invasion in North Africa until the final decision about opening the second front on the conference in Tehran in december 1943. In this period gradually prevailed the power of USA on the Grand strategy.
|
|
|
Analyzer of Windows Kernel Models
Calta, Jan ; Šerý, Ondřej (referee) ; Ježek, Pavel (advisor)
The thesis introduces a tool for analyzing models written in the specification language DeSpec and translating them into the Zing modeling language. Resulting models can be verified by the Zing model checker. The DeSpec language is designed primarily to specify the Windows NT kernel driver environment. It makes it possible to abstract this environment in the object-oriented way and it uses temporal logic patterns to capture rules imposed by the Windows kernel on drivers. The Zing language is designed to describe executable concurrent models of software, which can be explored by the Zing model checker. Properties to check are expressed by the assertions. So far, there has been no way to automatically extract a model from DeSpec specification and verify its properties by a model checker. The DeSpec-to-Zing compiler takes a crucial part in this task. The thesis demonstrates that it is feasible to translate DeSpec specifications into Zing models and that DeSpec is a suitable language for model checking of the Windows kernel driver environment. The introduced analyzer is capable to check correctness of DeSpec specifications and under the constrained conditions given by absence of other necessary tools it is capable to translate a subset of specifications into the Zing model.
|
guest ::
