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)]

Description in English
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.

Keywords
formální modely, simulační verifikace, formální verifikace, model checking

Key words in English
formal models, simulation verification, formal verification, model checking

GA102/07/0322

Czech

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

Department of Intelligent Systems
- responsible department (1.1.1989 - not assigned)
Automated Analysis and Verification Research Group - VeriFIT
- internal (1.2.2007 - 31.12.2009)
System Modelling and Optimization Research Group
- internal (1.2.2007 - 31.12.2009)
Department of Intelligent Systems
- co-beneficiary (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

Responsibility: Češka Milan, prof. RNDr., CSc.