Vysokoúrovňový návrh a formální verifikace jsou jednou z perspektivních cest, jak dosáhnout vyšší spolehlivosti a bezpečnosti počítačových systémů. Předkládaný projekt navazuje na zkušenosti a výsledky řešitelského týmu a na existující spolupráci se špičkovými zahraničními pracovišti a koncipuje základní výzkum takových pokročilých formálních přístupů, vycházejících z teorie systémů, logiky, teoretické informatiky a umělé inteligence, které jsou aplikovatelné v oblastech vysokoúrovňového návrhu a formální verifikace. Předpokládá, že tyto přístupy mohou výrazně pomoci tam, kde metody verifikace založené na hrubé síle selhávají. Projekt zahrnuje výzkum vzájemně se doplňujících metod návrhu založeného na modelech, simulační verifikaci a model checkingu konečně i nekonečně stavových systémů. Jedná se primárně o výzkum nových přístupů, metod a jejich vlastností, možných rozšíření či specializací apod. Metody vyvíjené v projektu budou prototypově implementovány a ověřeny na vhodných případových studiích. [private wiki (http://perchta.fit.vutbr.cz/intelligentsystems/103)]

Popis anglicky
High-level design and formal verification are promising approaches for improving reliability and safety of computer systems. This project is proposed by the highly experienced team with the expressive results and the international cooperation with the prestigious research teams. The project aims to explore and use advanced formal approaches from the fields like system theory, logics, theoretical computer science, and artificial intelligence in the area of the high-level design and formal verification. We believe that these approaches can significantly improve the verification abilities, especially in the cases on which the brute-force approach does not succeed. The proposed research project covers complementary methods, i.e., the model-driven design, the simulation-based verification, and the model checking of finite-state as well as infinite-state systems. The research should result in developing new approaches and methods with unique properties. These methods will be validated by the prototype implementation and will be evaluated by suitable case studies.

Klíčová slova
formální modely, simulační verifikace, formální verifikace, model checking

Klíčová slova anglicky
formal models, simulation verification, formal verification, model checking

GA102/07/0322

čeština

Češka Milan, prof. RNDr., CSc. - hlavní řešitel
Cerhák Michal, Ing. - spoluřešitel
Erlebach Pavel, Ing., Ph.D. - spoluřešitel
Holík Lukáš, doc. Mgr., Ph.D. - spoluřešitel
Janoušek Vladimír, doc. Ing., Ph.D. - spoluřešitel
Kironský Elöd, Ing. - spoluřešitel
Kočí Radek, Ing., Ph.D. - spoluřešitel
Křena Bohuslav, Ing., Ph.D. - spoluřešitel
Polášek Petr, Ing., Ph.D. - spoluřešitel
Rogalewicz Adam, doc. Mgr., Ph.D. - spoluřešitel
Smrčka Aleš, Ing., Ph.D. - spoluřešitel
Vojnar Tomáš, prof. Ing., Ph.D. - spoluřešitel

Ústav inteligentních systémů
- odpovědné pracoviště (1.1.1989 - nezadáno)
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT
- interní (1.2.2007 - 31.12.2009)
Výzkumná skupina modelování a optimalizace
- interní (1.2.2007 - 31.12.2009)
Ústav inteligentních systémů
- spolupříjemce (1.2.2007 - 31.12.2009)

HOLÍK, L. Simulations and Antichains for Efficient Handling of Finite Automata. Brno: Department of Intelligent Systems FIT BUT, 2011. p. 0-0.
Detail

HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; CHEN, Y. Mediating for Reduction (On Minimizing Alternating Büchi Automata). FIT-TR-2009-02, Brno: 2009. p. 0-0.
Detail

HOLÍK, L.; ŠIMÁČEK, J. Optimizing an LTS-Simulation Algorithm. FIT-TR-2009-03, Brno: 2009. p. 0-0.
Detail

ABDULLA, P.; HOLÍK, L.; CHEN, Y.; VOJNAR, T. Mediating for Reduction (On Minimizing Alternating Büchi Automata). Brno: Faculty of Information Technology BUT, 2009. p. 0-0.
Detail

IOSIF, R.; KONEČNÝ, F.; VOJNAR, T.; HABERMEHL, P.; BOZGA, M. Automatic Verification of Integer Array Programs. TR-2009-2, Grenoble: VERIMAG, 2009. p. 0-0.
Detail

LETKO, Z.; VOJNAR, T.; KŘENA, B.; NIR-BUCHBINDER, Y.; TZOREF-BRILL, R.; UR, S. A Concurrency Testing Tool and its Plug-ins for Dynamic Analysis and Runtime Healing. FIT-TR-2009-01, Brno: 2009. p. 0-0.
Detail

KŘENA, B.; BRAIONE, P.; DENARO, G.; PEZZE, M.: MUSE; Model checking Using Symbolic Execution. http://www.fit.vutbr.cz/research/groups/verifit/tools/muse/. URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/muse/. (software)
Detail

LETKO, Z.; VOJNAR, T.; KŘENA, B.: JRDH-AT; Java Atomicity Violation Detector & Healer. Nástroj i dokumentaci lze získat na URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/racedetect/. URL: https://www.fit.vut.cz/research/product/90/. (software)
Detail

KOČÍ, R.: PNtalk-08; PNtalk. Domovská stránka projektu (http://perchta.fit.vutbr.cz/pntalk2k/28). URL: https://www.fit.vut.cz/research/product/66/. (software)
Detail

ŠIMÁČEK, J.; HOLÍK, L.; VOJNAR, T.: SA; Tool for Computing Simulations. Nástroj i dokumentaci lze získat na URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/sa/. URL: https://www.fit.vut.cz/research/product/131/. (software)
Detail

KONEČNÝ, F.; VOJNAR, T.; BOZGA, M.; IOSIF, R.: FLATA; FLATA. http://www-verimag.imag.fr/FLATA.html. URL: http://www-verimag.imag.fr/FLATA.html. (software)
Detail

SMRČKA, A.: CDCreveal; Analyzátor CDC asynchronních komponent. http://www.fit.vutbr.cz/~smrcka/w/doku.php?id=research:cdcreveal. URL: http://www.fit.vutbr.cz/~smrcka/w/doku.php?id=research:cdcreveal. (software)
Detail

JANOUŠEK, V.; KIRONSKÝ, E.: SmallDEVS-07; SmallDEVS-07. http://www.fit.vutbr.cz/~janousek/smalldevs/. URL: http://www.fit.vutbr.cz/~janousek/smalldevs/. (software)
Detail

LETKO, Z.; VOJNAR, T.; KŘENA, B.: JRDH; Java Race Detector & Healer. Nástroj i dokumentaci lze získat na URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/racedetect/. URL: https://www.fit.vut.cz/research/product/49/. (software)
Detail

HABERMEHL, P.; VOJNAR, T. Proceedings of 10th International Workshop on Verification of Infinite-State Systems - INFINITY'08. Toronto: Faculty of Information Technology BUT, 2008. p. 0-0. ISBN: 978-80-214-3697-8.
Detail

HOLÍK, L.; VOJNAR, T.; BOUAJJANI, A.; HABERMEHL, P.; TOUILI, T. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. FIT-TR-2008-007, Brno: Faculty of Information Technology BUT, 2008. p. 0-0.
Detail

HABERMEHL, P.; IOSIF, R.; VOJNAR, T. What else is decidable about integer arrays?. TR-2007-8, Grenoble: VERIMAG, 2008. p. 0-0.
Detail

HABERMEHL, P.; IOSIF, R.; VOJNAR, T. A Logic of Singly Indexed Arrays. TR-2008-9, Grenoble: VERIMAG, 2008. p. 0-0.
Detail

HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; BOUAJJANI, A.; KAATI, L. Computing Simulations over Tree Automata: Efficient Techniques for Reducing Tree Automata. FIT-TR-2008-001, Brno: 2008. p. 0-0.
Detail

HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; KAATI, L. A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. FIT-TR-2008-005, Brno: 2008. p. 0-0.
Detail

Odpovědnost: Češka Milan, prof. RNDr., CSc.