Prejsť na obsah
dizertácie

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.

    Autoreferát dizertačnej práce 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.