Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail projektu
Období řešení: 01.09.2003 — 01.09.2006
Zdroje financování
Grantová agentura České republiky - Postdoktorandské granty
- plně financující (2003-09-01 - 2006-09-01)
O projektu
Neustálý růst složitosti počítačových systémů spolu s růstem nároků na jejich spolehlivost jsou příčinou, proč je v současnosti věnována značná pozornost vývoji automatizovaných metod a nástrojů pro rigorózní verifikaci jejich korektnosti. Mezi systémy, jimž je věnována zvláštní pozornost, patří protokoly počítačových a telekomunikačních sítí, paralelní software řídicích a operačních systémů, hardwarové komunikační protokoly apod. Zatímco pro případ, že uvažované systémy mají konečný stavový prostor, již byla vyvinuta řada poměrně efektivních verifikačních metod, automatická verifikace nekonečně stavových a parametrických systémů je mnohem méně rozpracovaná. Řada typů těchto systémů významných pro praxi není pokryta žádnými verifikačními metodami, případně metody, které jsou dostupné, nejsou příliš efektivní. Na základě zkušeností navrhovatele se současnými možnostmi a omezeními těchto metod předkládaný projekt usiluje o jejich rozvoj směrem k vyšší efektivitě a širší aplikovatelnosti. Důraz bude přitom kladen zejména na metody symbolické verifikace využívající automaty a převodníky pro práci s množinami stavů. Budou zkoumány možnosti použití nových typů automatů a také nové techniky pro efektivní manipulaci stávajících i nově uvažovaných typů automatů. Kromě zmíněných metod symbolické verifikace budou rozvíjeny rovněž metody řezů a automatizované abstrakce. Cílem projektu je přitom nejen teoretický výzkum, ale také prototypová implementace alespoň těch nejslibnějších z navržených metod.
Popis anglickyA constant growth in the complexity of computerized systems together with increasing demands on their reliability have currently lead to a strong interest in development of automated methods and tools for rigorous verification of correctness of such systems. Systems that attract a special attention include protocols of computer and telecommunication networks, concurrent software of control and operating systems, hardware communication protocols, etc. While many relatively efficient verification methods have been proposed for the case the considered systems have a finite state space, automatic verification of infinite-state and parametric systems is significantly less developed. Many practically important systems of this kind are not covered by any automatic verification methods, or the available methods are not very efficient. Based on experience of the applicant with current capabilities and restrictions of such methods, the proposed project aims at their further development towards higher efficiency and broader applicability. A special attention will be devoted to methods of symbolic verification based on using automata and transducers for handling sets of states. Possibilities of using new types of automata together with new techniques for efficient manipulation of the current as well as newly considered types of automata will be examined. Besides the mentioned methods of symbolic verification, methods based on cut-offs and automated abstraction will be explored too. The goal of the project is not only a theoretical research, but also a prototype implementation of at least the most promising approaches out of the proposed ones.
Klíčová slovaformální verifikace, model checking, parametrizované a nekonečně stavové systémy, paralelní systémy
Klíčová slova anglickyformal verification, model checking, parametric and infinite state systems, concurrent systems
Označení
GP102/03/D211
Originální jazyk
čeština
Řešitelé
Vojnar Tomáš, prof. Ing., Ph.D. - hlavní řešitelČeška Milan, prof. RNDr., CSc. - spoluřešitel
Útvary
Fakulta informačních technologií- příjemce (13.05.2004 - nezadáno)
Výsledky
JANOUŠEK, V., KOČÍ, R. Towards an Open Implementation of the PNtalk System. In Proceedings of the 5th EUROSIM Congress on Modeling and Simulation. Proceedings of the 5th Eurosim Congress on Modelling and Simulation. Paris: EUROSIM-FRANCOSIM-ARGESIM, 2004. p. 31-36. ISBN: 3-901608-28-1.Detail
NOVOSAD, P.; ČEŠKA, M. Algorithm for Computing Unfoldings of Unbounded Hybrid Petri Nets. Computer Aided System Theory -EUROCAST 2013 - revised selected papers. Lecture Notes in Computer Science. Berín: Springer Verlag, 2013. p. 428-435. ISBN: 978-3-642-53855-1.Detail
ERLEBACH, P. Experience from Verifying in TVLA. In EEICT'05. volume 3. Brno: Faculty of Electrical Engineering and Communication BUT, 2005. p. 648-652. ISBN: 80-214-2890-2.Detail
VOJNAR, T., ČEŠKA, M., ERLEBACH, P. Pattern-Based Verification of Programs with Extended Linear Linked Data Structures. In Proceedings of Fifth International Workshop on Automated Verification of Critical Systems. Warwick: 2005. p. 101-117.Detail
ERLEBACH, P. Towards a Systematic Framework for Automatic Pattern-Based Verification of Dynamic Data Structures. In PRE-PROCEEDINGS of the 1st Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Brno: Faculty of Informatics MU, 2005. p. 145-154.Detail
ERLEBACH, P., VOJNAR, T. Automated Formal Verification of Programs with Dynamic Data Structures Using State-of-the-Art Tools. In Proceedings of 8th International Conference ISIM'05 Information System Implementation and Modeling. Ostrava: 2005. p. 219-226. ISBN: 80-86840-09-3.Detail
ROGALEWICZ, A. Towards Applying Mona in Abstract Regular Tree Model Checking. In Proceedings of the 11th Conference Student EEICT 2005. Volume 3. Brno: Faculty of Information Technology BUT, 2005. p. 663-667. ISBN: 80-214-2890-2.Detail
BOUAJJANI, A., HABERMEHL, P., ROGALEWICZ, A., VOJNAR, T. Abstract Regular Tree Model Checking. In Proceedings of 7th International Workshop on Verification of Infinite-State Systems -- INFINITY 2005. BRICS Notes Series. Aarhus: Basic Research in Computer Science, Computer Science Departments of the Aarlborg and Aarhus Universities, 2005. p. 15-24. ISSN: 0909-3206.Detail
KŘENA, B., ČEŠKA, M., VOJNAR, T. Parallel State Space Generation and Exploration on Shared-Memory Architectures. In Computer Aided Systems Theory - EUROCAST 2005. Lecture Notes in Computer Science 3643. Berlin: Springer Verlag, 2005. p. 275-280. ISBN: 978-3-540-29002-5.Detail
BOUAJJANI, A.; HABERMEHL, P.; ROGALEWICZ, A.; VOJNAR, T. Abstract Regular Tree Model Checking of Complex Dynamic Data Structures. In Static Analysis. LNCS 4134. Berlin: Springer Verlag, 2006. p. 52-70. ISBN: 978-3-540-37756-6.Detail
HABERMEHL, P.; IOSIF, R.; VOJNAR, T. Automata-based Verification of Programs with Tree Updates. In Tools and Algorithms for the Construction and Analysis of Systems. LNCS 3920. Berlin: Springer Verlag, 2006. p. 350-364. ISBN: 978-3-540-33056-1.Detail
VOJNAR, T., BOUAJJANI, A., HABERMEHL, P., MORO, P. Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. In Tools and Algorithms for the Construction and Analysis of Systems. LNCS 3440. Berlin: Springer Verlag, 2005. p. 13-29. ISBN: 978-3-540-25333-4.Detail
VOJNAR, T.; ČEŠKA, M.; ERLEBACH, P. Pattern-Based Verification of Programs with Extended Linear Linked Data Structures. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, vol. 2006, no. 145, p. 113-130. ISSN: 1571-0661.Detail
BOUAJJANI, A.; HABERMEHL, P.; ROGALEWICZ, A.; VOJNAR, T. Abstract Regular Tree Model Checking. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, vol. 149, no. 1, p. 37-48. ISSN: 1571-0661.Detail
HABERMEHL, P., VOJNAR, T. Regular Model Checking Using Inference of Regular Languages. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, vol. 138, no. 3, p. 21-36. ISSN: 1571-0661.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
BOUAJJANI, A., HABERMEHL, P., VOJNAR, T. Abstract Regular Model Checking. Lecture Notes in Computer Science, 2004, vol. 2004, no. 3114, p. 372-386. ISSN: 0302-9743.Detail
HABERMEHL, P., RADU, I., VOJNAR, T. Automata-based Verification of Programs with Tree Updates. Verimag Technical Report number TR-2005-16, Grenoble: VERIMAG, 2005.Detail
ROGALEWICZ, A. Verification of Programs with Complex Data Structures. Brno: 2007. 122 p. ISBN: 978-80-214-3548-3.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
NOVOSAD, P.; ČEŠKA, M. Algorithm for Computing Unfoldings of Unbounded Hybrid Petri Nets. Proc. of Computer Aided System Theory 2013. Universidad de Las Palmas de Gran Canaria: The Universidad de Las Palmas de Gran Canaria, 2013. p. 244-245. ISBN: 84-695-6971-6.Detail
ROGALEWICZ, A., VOJNAR, T. Tree Automata In Modelling And Verification Of Concurrent Programs. In Proceedings of ASIS 2004. Ostrava: 2004. p. 197-202. ISBN: 80-86840-03-4.Detail