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: Postdoktorandské granty

Název anglicky
Advanced Methods of Automatic Verification of Parametric and Infinite-State Systems
Typ
grant
Klíčová slova

formální verifikace, model checking, parametrizované a nekonečně stavové systémy,
paralelní systémy

Abstrakt

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šitelé
Vojnar Tomáš, prof. Ing., Ph.D. (UITS) – hlavní řešitel
Češka Milan, prof. RNDr., CSc.
Publikace

2013

  • 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
  • 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

2007

  • 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
  • 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

2006

  • BOUAJJANI, A.; HABERMEHL, P.; ROGALEWICZ, A.; VOJNAR, T. Abstract Regular Tree Model Checking of Complex Dynamic Data Structures. Static Analysis. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2006. p. 52-70. ISBN: 978-3-540-37756-6. 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.; IOSIF, R.; VOJNAR, T. Automata-based Verification of Programs with Tree Updates. Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2006. p. 350-364. ISBN: 978-3-540-33056-1. 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

2005

  • BOUAJJANI, A.; HABERMEHL, P.; ROGALEWICZ, A.; VOJNAR, T. Abstract Regular Tree Model Checking. 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
  • ERLEBACH, P. Experience from Verifying in TVLA. EEICT'05. volume 3. Brno: Faculty of Electrical Engineering and Communication BUT, 2005. p. 648-652. ISBN: 80-214-2890-2. Detail
  • ERLEBACH, P. Towards a Systematic Framework for Automatic Pattern-Based Verification of Dynamic Data Structures. PRE-PROCEEDINGS of the 1st Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Brno: Faculty of Informatics MU, 2005. p. 145-154. ISBN: 0. Detail
  • ERLEBACH, P.; VOJNAR, T. Automated Formal Verification of Programs with Dynamic Data Structures Using State-of-the-Art Tools. Proceedings of 8th International Conference ISIM'05 Information System Implementation and Modeling. Ostrava: 2005. p. 219-226. ISBN: 80-86840-09-3. 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
  • 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
  • KŘENA, B.; ČEŠKA, M.; VOJNAR, T. Parallel State Space Generation and Exploration on Shared-Memory Architectures. Computer Aided Systems Theory - EUROCAST 2005. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2005. p. 275-280. ISBN: 978-3-540-29002-5. Detail
  • ROGALEWICZ, A. Towards Applying Mona in Abstract Regular Tree Model Checking. 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
  • VOJNAR, T.; BOUAJJANI, A.; HABERMEHL, P.; MORO, P. Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. 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. Proceedings of Fifth International Workshop on Automated Verification of Critical Systems. Warwick: 2005. p. 101-117. Detail

2004

  • 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.; VOJNAR, T. Regular Model Checking Using Inference of Regular Languages. Proceedings of 6th International Workshop on Verification of Infinite-State Systems -- INFINITY 2004. London: 2004. p. 61-71. Detail
  • JANOUŠEK, V.; KOČÍ, R. Towards an Open Implementation of the PNtalk System. 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
  • ROGALEWICZ, A.; VOJNAR, T. Tree Automata In Modelling And Verification Of Concurrent Programs. Proceedings of ASIS 2004. Ostrava: 2004. p. 197-202. ISBN: 80-86840-03-4. Detail

2003

  • BOUAJJANI, A.; HABERMEHL, P.; VOJNAR, T. Verification of Parametric Concurrent Systems with Prioritized FIFO Resource Management. Lecture Notes in Computer Science, 2003, vol. 2003, no. 2761, p. 174-190. ISSN: 0302-9743. Detail
Nahoru