Detail projektu

Pokročilé formální přístupy v návrhu a automatické verifikaci počítačových systémů

Období řešení: 01.01.2007 — 31.12.2009

Zdroje financování

Grantová agentura České republiky - Standardní projekty

- plně financující (2007-01-01 - 2009-12-31)

O projektu

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]

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

Označení

GA102/07/0322

Originální jazyk

čeština

Řešitelé

Č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

Útvary

Ústav inteligentních systémů
- spolupříjemce (01.01.2007 - 31.12.2009)

Výsledky

HRUBÁ, V.; KŘENA, B.; VOJNAR, T. Using JavaPathFinder for Self-healing Assurance. In Proceedings of 3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science - MEMICS 2007. Znojmo: Ing. Zdeněk Novotný, CSc., 2007. p. 67-73. ISBN: 978-80-7355-077-6.
Detail

JANOUŠEK, V.; KIRONSKÝ, E.; POLÁŠEK, P. An Architecture for Simulation-Based Evolutionary Design of Systems. In Proceedings of the 16th International Conference on System Science. Systems Science 2007, volume 1. Wroclaw: Wroclaw University of Technology, 2007. p. 396-405. ISBN: 978-83-7493-339-1.
Detail

VOJNAR, T. Stromové automaty s omezeními v symbolické verifikaci programů manipulujících vyvážené stromy. In Současné trendy teoretické informatiky. ITI Series 2007-347. Praha: 2007. s. 38-39.
Detail

KOČÍ, R.; MAZAL, Z.; ZBOŘIL, F.; JANOUŠEK, V. Modeling Deliberative Agents Using Object Oriented Petri Nets. In Proceedings of the 7th ISDA. Los Alamitos: IEEE Computer Society, 2007. p. 15-20. ISBN: 0-7695-2976-3.
Detail

ZBOŘIL, F.; KOČÍ, R. Intention Structures Modelling Using Object Oriented Petri Nets. In Proceedings of the 7th ISDA. Los Alamitos: IEEE Computer Society, 2007. p. 33-38. ISBN: 0-7695-2976-3.
Detail

ERLEBACH, P.; ČEŠKA, M.; VOJNAR, T. Pattern-Based Verification for Trees. In Computer Aided Systems Theory - EUROCAST 2007. Las Palmas de Grand Canaria: The Universidad de Las Palmas de Gran Canaria, 2007. p. 181-182. ISBN: 978-3-540-75866-2.
Detail

KŘENA, B.; LETKO, Z.; TZOREF-BRILL, R.; UR, S.; VOJNAR, T. Healing Data Races On-The-Fly. In Proceedings of 5th International Workshop on Parallel and Distributed Systems: Testing and Debugging Modelling - PADTAD'07. London: Association for Computing Machinery, 2007. p. 54-64. ISBN: 978-1-59593-734-6.
Detail

JANOUŠEK, V.; KOČÍ, R. Embedding Object-Oriented Petri Nets into a DEVS-based Simulation Framework. In Proceedings of the 16th International Conference on System Science. volume 1. Wroclaw: Wroclaw University of Technology, 2007. p. 386-395. ISBN: 978-83-7493-339-1.
Detail

JANOUŠEK, V.; KOČÍ, R. Simulation and Design of Systems with Object Oriented Petri Nets. In Proceedings of the 6th EUROSIM Congress on Modelling and Simulation. Ljubljana: ARGE Simulation News, 2007. p. 1-9. ISBN: 978-3-901608-32-2.
Detail

DUDKA, V.; VOJNAR, T.; KŘENA, B. Self-healing Assurance using Bounded Model Checking. Computer Aided Systems Theory. Las Palmas de Grand Canaria: The Universidad de Las Palmas de Gran Canaria, 2009. p. 99-100. ISBN: 978-84-691-8502-5.
Detail

KOČÍ, R.; JANOUŠEK, V. On the Dynamic Features of PNtalk. International Workshop on Petri Nets and Software Engineering 2009. Paříž: University of Pierre and Marie Curie, 2009. p. 189-206.
Detail

IOSIF, R.; ROGALEWICZ, A. Automata-Based Termination Proofs. Implementation and Application of Automata. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2009. p. 165-177. ISBN: 978-3-642-02978-3.
Detail

KOČÍ, R.; JANOUŠEK, V. Towards Simulation-Based Design of the Software Systems. The Fourth International Conference on Software Engineering Advances. Los Alamitos: IEEE Computer Society, 2009. p. 452-457. ISBN: 978-1-4244-4779-4.
Detail

MAZAL, Z.; JANOUŠEK, V.; KOČÍ, R. Enhancing the PNtalk Language with Negative Predicates. MOSIS '08. Ostrava: 2008. p. 28-34. ISBN: 978-80-86840-40-6.
Detail

JANOUŠEK, V.; KIRONSKÝ, E. Reflective Framework for Interactive Modeling and Simulation of Intelligent Systems. Proceedings of Nineteenth International Conference on Systems Engineering 19-21 August 2008 Las Vegas, Nevada. Los Alamitos: IEEE Computer Society, 2008. p. 480-485. ISBN: 978-0-7695-3331-5.
Detail

LETKO, Z.; VOJNAR, T.; KŘENA, B. AtomRace: data race and atomicity violation detector and healer. PADTAD '08. Proceedings of the 6th workshop on Parallel and distributed systems. Seattle: Association for Computing Machinery, 2008. p. 1-10. ISBN: 978-1-60558-052-4.
Detail

JANOUŠEK, V.; KOČÍ, R.; MAZAL, Z.; ZBOŘIL, F. PNagent: a Framework for Modelling BDI Agents using Object Oriented Petri Nets. Proceedings of 8th ISDA. Los Alamitos: IEEE Computer Society, 2008. p. 420-425. ISBN: 978-0-7695-3382-7.
Detail

NOVOSAD, P.; ČEŠKA, M. Algorithms for Computing Coverability Graphs for Hybrid Petri Nets. 4th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Brno: Masaryk University, 2008. p. 177-183. ISBN: 978-80-7355-082-0.
Detail

HABERMEHL, P.; IOSIF, R.; VOJNAR, T. What else is decidable about integer arrays?. Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2008. p. 475-490. ISBN: 978-3-540-78497-5.
Detail

HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; BOUAJJANI, A.; KAATI, L. Computing Simulations over Tree Automata (Efficient Techniques for Reducing Tree Automata). Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2008. p. 93-108. ISBN: 978-3-540-78799-0.
Detail

IOSIF, R.; KONEČNÝ, F.; VOJNAR, T.; HABERMEHL, P.; BOZGA, M. Automatic Verification of Integer Array Programs. Computer Aided Verification. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2009. p. 157-172. ISBN: 978-3-642-02657-7.
Detail

KŘENA, B.; LETKO, Z.; VOJNAR, T.; NIR-BUCHBINDER, Y.; TZOREF-BRILL, R.; UR, S. A Concurrency Testing Tool and Its Plug-Ins for Dynamic Analysis and Runtime Healing. Runtime Verification. Lecture Notes in Computer Science, Volume 5779/2009. Berlin: Springer Verlag, 2009. p. 101-114. ISBN: 978-3-642-04693-3.
Detail

HOLÍK, L.; ŠIMÁČEK, J. Optimizing an LTS-Simulation Algorithm. 5th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Znojmo: Faculty of Informatics MU, 2009. p. 93-101. ISBN: 978-3-939897-15-6.
Detail

HABERMEHL, P.; IOSIF, R.; ROGALEWICZ, A.; VOJNAR, T. Proving Termination of Tree Manipulating Programs. In Automated Technology for Verification and Analysis. LNCS 4762. Berlin: Springer Verlag, 2007. p. 145-161. ISBN: 978-3-540-75595-1.
Detail

ERLEBACH, P.; VOJNAR, T.; ČEŠKA, M. Pattern-based Verification for Trees. In Computer Aided Systems Theory. LNCS 4739. Berlin: Springer Verlag, 2007. p. 488-496. ISBN: 978-3-540-75866-2.
Detail

HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; CHEN, Y. Zprostředkování pro redukci (Za minimalizací alternujících automatů). IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009). LIPIcs, sv. 4. Wadern: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2009. s. 1-12. ISBN: 978-3-939897-13-2.
Detail

KOČÍ, R.; JANOUŠEK, V.; ZBOŘIL, F. Object Oriented Petri Nets -- Modelling Techniques Case Study. Second UKSIM European Symposium on Computer Modeling and Simulation. Liverpool: IEEE Computer Society, 2008. p. 165-170. ISBN: 978-0-7695-3325-4.
Detail

JANOUŠEK, V.; KOČÍ, R. The PNtalk/SmallDEVS Framework -- Meta-level Modeling Techniques. Proceedings of CSE 2008 International Scientific Conference on Computer Science and Engineering. Košice: elfa, s.r.o., TU Kosice, 2008. p. 16-23. ISBN: 978-80-8086-092-9.
Detail

KOČÍ, R.; JANOUŠEK, V. System Design with Object Oriented Petri Nets Formalism. The Third International Conference on Software Engineering Advances Proceedings ICSEA 2008. Los Alamitos: IEEE Computer Society, 2008. p. 421-426. ISBN: 978-0-7695-3372-8.
Detail

SKLENÁŘ, J.; CUTARAJ, V.; ČEŠKA, M. Using Integer Programming for Discrete Problem Optimization. The 2008 European Simulation and Modelling Conference. EUROSIS-ETI Publications. LE HAVRE: EUROSIM-FRANCOSIM-ARGESIM, 2008. p. 19-21. ISBN: 978-90-77381-44-1.
Detail

POLÁŠEK, P.; JANOUŠEK, V. Modeling and Simulation Management in Distributed Environment Using Web Services. Proceedings of the 14th International Congress of Cybernetics and Systems of WOCS. Wroclaw: Wroclaw University of Technology, 2008. p. 1-9. ISBN: 978-83-7493-400-8.
Detail

LETKO, Z. An Architecture for Self-Healing of Data Races and Atomicity Violations for Java. Proceedings of the 14th Conference STUDENT EEICT 2008. Volume 2. Brno: Brno University of Technology, 2008. p. 256-258. ISBN: 978-80-214-3615-2.
Detail

DUDKA, V. Bounded Model Checking Using Java PathFinder. Proceedings of the 14th Conference STUDENT EEICT 2008. Volume 2. Brno: Brno University of Technology, 2008. p. 247-249. ISBN: 978-80-214-3615-2.
Detail

HÝSEK, J. Visual design of SmallDEVS models using statecharts. Proceedings of ASIS 2008. Rožnov pod Radhoštěm: Czech Science Foundation, 2008. p. 999-1004. ISBN: 978-80-86840-42-0.
Detail

KOČÍ, R.; JANOUŠEK, V. Simulation Based Design of Control Systems Using DEVS and Petri Nets. Computer Aided Systems Theory - EUROCAST 2009. Lecture Notes in Computer Science, Volume 5717. Berlin: Springer Verlag, 2009. p. 849-856. ISBN: 978-3-642-04771-8.
Detail

HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; KAATI, L. A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. 4th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Brno: Faculty of Informatics MU, 2008. p. 3-11. ISBN: 978-80-7355-082-0.
Detail

NOVOSAD, P.; ČEŠKA, M. Algorithms for Computing Coverability Graphs for Continuous Petri Nets. Proceedings of 22th European Simulation and Modelling Conference ESM'2008. EUROSIS-ETI Publications. Le Havre: EUROSIM-FRANCOSIM-ARGESIM, 2008. p. 489-491. ISBN: 978-90-77381-44-1.
Detail

JANOUŠEK, V.; KVĚTOŇOVÁ, Š. On the Multilevel Petri Nets-Based Models in Project Engineering. International Workshop on Petri Nets and Software Engineering 2009. Paříž: University of Pierre and Marie Curie, 2009. p. 173-188.
Detail

HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; BOUAJJANI, A.; KAATI, L. Composed Bisimulation for Tree Automata. Implementation and Application of Automata. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2008. p. 212-222. ISBN: 978-3-540-70843-8.
Detail

HOLÍK, L.; VOJNAR, T.; BOUAJJANI, A.; HABERMEHL, P.; TOUILI, T. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. Implementation and Application of Automata. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2008. p. 57-67. ISBN: 978-3-540-70843-8.
Detail

IOSIF, R.; VOJNAR, T.; HABERMEHL, P. A Logic of Singly Indexed Arrays. Logic for Programming, Artificial Intelligence and Reasoning. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2008. p. 558-573. ISBN: 978-3-540-89438-4.
Detail

DUDKA, V.; KŘENA, B.; VOJNAR, T. Self-healing Assurance using Bounded Model Checking. Computer Aided Systems Theory - EUROCAST 2009. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2009. p. 295-303. ISBN: 978-3-642-04771-8.
Detail

BOZGA, M.; IOSIF, R.; KONEČNÝ, F. Fast Acceleration of Ultimately Periodic Relations. Computer Aided Verification. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2010. p. 227-242. ISBN: 978-3-642-14294-9.
Detail

ERLEBACH, P.; ČEŠKA, M.; VOJNAR, T. Generalised Multi-Pattern-Based Verification of Programs with Linear Linked Structures. Formal Aspects of Computing, 2007, vol. 19, no. 3, p. 363-374. ISSN: 0934-5043.
Detail

MAZAL, Z.; KOČÍ, R.; JANOUŠEK, V.; ZBOŘIL, F. Modelling intelligent agents for autonomic computing in the PNagent framework. International Journal of Autonomic Computing, 2009, vol. 1, no. 2, p. 121-139. ISSN: 1741-8569.
Detail

JANOUŠEK, V.; KIRONSKÝ, E. Interactive evolutionary modelling and simulation of discrete-event systems using prototypical objects. International Journal of Autonomic Computing, 2009, vol. 1, no. 2, p. 104-120. ISSN: 1741-8569.
Detail

HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; BOUAJJANI, A.; KAATI, L. Composed Bisimulation for Tree Automata. International Journal of Foundations of Computer Science, 2009, vol. 20, no. 4, p. 685-700. ISSN: 0129-0541.
Detail

VOJNAR, T.; ČEŠKA, M.; ROGALEWICZ, A.; ERLEBACH, P.; HOLÍK, L.; BOUAJJANI, A.; HABERMEHL, P.; TOUILI, T.; MORO, P. Automatická verifikace programů s dynamickými datovými strukturami. Inovační podnikání & transfer technologií, 2008, roč. 2008, č. 1, s. 21-22. ISSN: 1210-4612.
Detail

VOJNAR, T.; HABERMEHL, P.; BOUAJJANI, A. Verification of parametric concurrent systems with prioritised FIFO resource management. FORMAL METHODS IN SYSTEM DESIGN, 2008, vol. 32, no. 2, p. 129-172. ISSN: 0925-9856.
Detail

HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; KAATI, L. A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, vol. 2009, no. 251, p. 27-48. ISSN: 1571-0661.
Detail

IOSIF, R.; VOJNAR, T.; HABERMEHL, P. Automata-based Verification of Programs with Tree Updates. Acta Informatica, 2010, vol. 47, no. 1, p. 1-31. ISSN: 0001-5903.
Detail

KOČÍ, R.; JANOUŠEK, V.; ZBOŘIL, F. Object Oriented Petri Nets - Modelling Techniques Case Study. International Journal of Simulation Systems, Science & Technology, 2010, vol. 10, no. 3, p. 32-44. ISSN: 1473-8031.
Detail

VOJNAR, T. Cut-offs and Automata in Formal Verification of Infinite-State Systems. FIT Monograph 1. FIT Monograph 1. Brno: Faculty of Information Technology BUT, 2007. 189 p. ISBN: 978-80-214-3547-6.
Detail

HOLÍK, L., VOJNAR, T., ABDULLA, P., BOUAJJANI, A., KAATI, L. Composed Bisimulation for Tree Automata. FIT-TR-2008-004, Brno: 2008.
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.
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.
Detail

HABERMEHL, P., RADU, I., VOJNAR, T. A Logic of Singly Indexed Arrays. TR-2008-9, Grenoble: VERIMAG, 2008.
Detail

HABERMEHL, P., RADU, I., VOJNAR, T. What else is decidable about integer arrays?. TR-2007-8, Grenoble: VERIMAG, 2008.
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.
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

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

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

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

Š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

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

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

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

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