Detail projektu
Pokročilé metody automatické verifikace parametrických a nekonečně stavových systémů
Období řešení: 1. 9. 2003 - 1. 9. 2006
Typ projektu: grant
Kód: GP102/03/D211
Agentura: Grantová agentura České republiky
Program:
formální verifikace, model checking, parametrizované a nekonečně stavové systémy, paralelní systémy
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.
Češka Milan, prof. RNDr., CSc. (UITS FIT VUT) , spoluřešitel
2013
- NOVOSAD Petr a ČEŠKA Milan. Algorithm for Computing Unfoldings of Unbounded Hybrid Petri Nets. In: Proc. of Computer Aided System Theory 2013. Universidad de Las Palmas de Gran Canaria: Universidad de Las Palmas de Gran Canaria, 2013, s. 244-245. ISBN 84-695-6971-6. Detail
- NOVOSAD Petr a ČEŠKA Milan. Algorithm for Computing Unfoldings of Unbounded Hybrid Petri Nets. In: Computer Aided System Theory -EUROCAST 2013 - revised selected papers. Lecture Notes in Computer Science. Berín: Springer Verlag, 2013, s. 428-435. ISBN 978-3-642-53855-1. Detail
2007
- VOJNAR Tomáš. Cut-offs and Automata in Formal Verification of Infinite-State Systems. FIT Monograph 1. Brno: Fakulta informačních technologií VUT v Brně, 2007. ISBN 978-80-214-3547-6. Detail
- ČEŠKA Milan, ERLEBACH Pavel a VOJNAR Tomáš. Generalised Multi-Pattern-Based Verification of Programs with Linear Linked Structures. Formal Aspects of Computing, roč. 19, č. 3, 2007, s. 363-374. ISSN 0934-5043. Detail
- ROGALEWICZ Adam. Verification of Programs with Complex Data Structures. Brno, 2007. ISBN 978-80-214-3548-3. Detail
2006
- BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam a VOJNAR Tomáš. Abstract Regular Tree Model Checking. Electronic Notes in Theoretical Computer Science, roč. 149, č. 1, 2006, s. 37-48. ISSN 1571-0661. Detail
- BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam a VOJNAR Tomáš. Abstract Regular Tree Model Checking of Complex Dynamic Data Structures. In: Static Analysis. Lecture Notes in Computer Science, roč. 4134. Berlin: Springer Verlag, 2006, s. 52-70. ISBN 978-3-540-37756-6. Detail
- HABERMEHL Peter, IOSIF Radu a VOJNAR Tomáš. Automata-based Verification of Programs with Tree Updates. In: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, roč. 3920. Berlin: Springer Verlag, 2006, s. 350-364. ISBN 978-3-540-33056-1. Detail
- ČEŠKA Milan, ERLEBACH Pavel a VOJNAR Tomáš. Pattern-Based Verification of Programs with Extended Linear Linked Data Structures. Electronic Notes in Theoretical Computer Science, roč. 2006, č. 145, s. 113-130. ISSN 1571-0661. Detail
2005
- BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam a VOJNAR Tomáš. Abstract Regular Tree Model Checking. In: Proceedings of 7th International Workshop on Verification of Infinite-State Systems -- INFINITY 2005. Aarhus: Basic Research in Computer Science, Computer Science Departments of the Aarlborg and Aarhus Universities, 2005, s. 15-24. ISSN 0909-3206. Detail
- HABERMEHL Peter, IOSIF Radu a VOJNAR Tomáš. Automata-based Verification of Programs with Tree Updates. Verimag Technical Report number TR-2005-16, Grenoble: VERIMAG, 2005. Detail
- ERLEBACH Pavel a VOJNAR Tomáš. 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: MARQ, 2005, s. 219-226. ISBN 80-86840-09-3. Detail
- ERLEBACH Pavel. Experience from Verifying in TVLA. In: EEICT'05. volume 3. Brno: Fakulta elektrotechniky a komunikačních technologií VUT v Brně, 2005, s. 648-652. ISBN 80-214-2890-2. Detail
- ČEŠKA Milan, KŘENA Bohuslav a VOJNAR Tomáš. Parallel State Space Generation and Exploration on Shared-Memory Architectures. In: Computer Aided Systems Theory - EUROCAST 2005. Lecture Notes in Computer Science, roč. 3643. Berlin: Springer Verlag, 2005, s. 275-280. ISBN 978-3-540-29002-5. Detail
- ČEŠKA Milan, ERLEBACH Pavel a VOJNAR Tomáš. 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, s. 101-117. Detail
- HABERMEHL Peter a VOJNAR Tomáš. Regular Model Checking Using Inference of Regular Languages. Electronic Notes in Theoretical Computer Science, roč. 138, č. 3, 2005, s. 21-36. ISSN 1571-0661. Detail
- ERLEBACH Pavel. 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: Fakulta informatiky MU, 2005, s. 145-154. Detail
- ROGALEWICZ Adam. Towards Applying Mona in Abstract Regular Tree Model Checking. In: Proceedings of the 11th Conference Student EEICT 2005. Volume 3. Brno: Fakulta informačních technologií VUT v Brně, 2005, s. 663-667. ISBN 80-214-2890-2. Detail
- BOUAJJANI Ahmed, HABERMEHL Peter, MORO Pierre a VOJNAR Tomáš. Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. In: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, roč. 3440. Berlin: Springer Verlag, 2005, s. 13-29. ISBN 978-3-540-25333-4. Detail
2004
- BOUAJJANI Ahmed, HABERMEHL Peter a VOJNAR Tomáš. Abstract Regular Model Checking. Lecture Notes in Computer Science, roč. 2004, č. 3114, s. 372-386. ISSN 0302-9743. Detail
- HABERMEHL Peter a VOJNAR Tomáš. Regular Model Checking Using Inference of Regular Languages. In: Proceedings of 6th International Workshop on Verification of Infinite-State Systems -- INFINITY 2004. London, 2004, s. 61-71. Detail
- ROGALEWICZ Adam a VOJNAR Tomáš. Tree Automata In Modelling And Verification Of Concurrent Programs. In: Proceedings of ASIS 2004. Ostrava: MARQ, 2004, s. 197-202. ISBN 80-86840-03-4. Detail
2003
- BOUAJJANI Ahmed, HABERMEHL Peter a VOJNAR Tomáš. Verification of Parametric Concurrent Systems with Prioritized FIFO Resource Management. Lecture Notes in Computer Science, roč. 2003, č. 2761, s. 174-190. ISSN 0302-9743. Detail