Dovoľujeme si oznámiť, že dňa
23. 9. 2010 o 11:00
sa bude konať na Fakulte informatiky a informačných technológií STU v Bratislave
v miestnosti D 220 obhajoba dizertačnej práce
Ing. Daniely Kotmanovej
Názov dizertačnej práce:
Temporálne špecifikácie vo verifikácii digitálnych systémov
Odbor: 9.2.9 Aplikovaná informatika
Školiteľ: doc. Ing. Ladislav Hudec, PhD., Fakulta informatiky a informačných technológií STU v Bratislave
Oponenti dizertačnej práce:
prof. Ing. Štefan Hudák, DrSc., Fakulta elektrotechniky a informatiky TU v Košiciach
doc. RNDr. Jaroslav Fogel, CSc. Fakulta elektrotechniky a informatiky STU v Bratislave
Abstrakt:
Predložená práca sa zaoberá využitím neklasických logík vo verifikácii digitálnych systémov. Zamerali sme sa najmä na nájdenie spôsobu, ako zostavovať’ temporálne špecifikácie popisujúce správanie digitálnych modelov v softvérovom prostredí model checkera SMV. V hlavnej časti práce prezentujeme navrhnutú metodiku, ktorá umožni špecifikovať’ synchrónne sekvenčné obvody a kombinačné obvody a následne ich verifikovať’. Metodika je znázornená vo forme diagramu s podrobne okomentovanými zložkami. Cely postup sme názorne ilustrovali na vzorovom príklade, ktorý sme navrhli, vyšpecifikovali a verifikovali krok za krokom podľa navrhnutého postupu. Ďalej sme navrhli formulu na prevod digitálneho modelu s abstrakciou na úrovni konečného automatu na Kripkeho štruktúru, ktorá je podľa našich zistení v tomto prípade identická so stavovo-priestorovým modelom.
V experimentálnej časti práce sa zameriavame na overovanie navrhnutej metodiky na známych modeloch digitálnych obvodov a aplikáciu navrhnutej metodiky na úplne nové modely. Konkrétne obvody sme navrhli, popísali dynamické správanie modelu, vyjadrili temporálne špecifikácie a napísali verifikačný program. V prílohách sú uvedené všetky verifikačné programy, okná výsledkov a výstupné súbory.
V Dodatku sme porovnali charakter jednotlivých neklasických logík a ich vzťah ku klasickej predikátovej logike.
The thesis studies the applications of non-classical logics in the verification of digital systems. We focused mainly on finding how to establish temporal specifications describing digital model behaviour using a model checker SMV as a software verification tool. In the main part of our thesis we propose a method intended for use in synchronous sequential and combinational digital circuit designs in order to verify them. Our method is presented in the form of a diagram with parts that are explained
in detail. The method is illustrated through the example of a digicode we have designed, specified and verified step by step according to the proposed method. Further, we provide a formula to transform a digital model with an abstraction on the finite state machine level to the Kripke structure, which is, as we found out, identical in this case to the state space model.
In the experimental part of our thesis, we focus first on testing the method on several digital circuit designs and after that, on applying the proposed method on wholly new models. Concrete circuits have been designed, their dynamic behaviour has been described, temporal specifications have been expressed and finally, a verification program has been written. The joint Appendix contains all of the verification programs, result windows and output files.
In the Supplement, we compare the character of non-classical logics and their relation to the classical predicate logic.
zaslaný do vedeckého časopisu Information Sciences and Technologies - Bulletin of ACM Slovakia
Dizertačná práca je k nahliadnutiu na Študijnom oddelení FIIT STU.