Detail projektu

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

Období řešení: 1. 1. 2007 - 31. 12. 2009

Typ projektu: grant

Kód: GA102/07/0322

Agentura: Grantová agentura České republiky

Program:

Název anglicky
Advanced Formal Approaches in the Design and Verification of Computer-Based Systems
Typ
grant
Klíčová slova

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

Abstrakt

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]

Řešitelé
Češka Milan, prof. RNDr., CSc. (UITS FIT VUT) , hlavní řešitel
Cerhák Michal, Ing. (UITS FIT VUT) , spoluřešitel
Erlebach Pavel, Ing. (UITS FIT VUT) , spoluřešitel
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT) , spoluřešitel
Janoušek Vladimír, doc. Ing., Ph.D. (UITS FIT VUT) , spoluřešitel
Kironský Elöd, Ing. (UITS FIT VUT) , spoluřešitel
Kočí Radek, Ing., Ph.D. (UITS FIT VUT) , spoluřešitel
Křena Bohuslav, Ing., Ph.D. (UITS FIT VUT) , spoluřešitel
Polášek Petr, Ing. (UITS FIT VUT) , spoluřešitel
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT) , spoluřešitel
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT) , spoluřešitel
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT) , spoluřešitel
Publikace

2010

  • HABERMEHL Peter, IOSIF Radu a VOJNAR Tomáš. Automata-based Verification of Programs with Tree Updates. Acta Informatica, roč. 47, č. 1, 2010, s. 1-31. ISSN 0001-5903. Detail
  • BOZGA Marius, IOSIF Radu a KONEČNÝ Filip. Fast Acceleration of Ultimately Periodic Relations. In: Computer Aided Verification. Lecture Notes in Computer Science, roč. 6174. Berlin: Springer Verlag, 2010, s. 227-242. ISBN 978-3-642-14294-9. Detail
  • KOČÍ Radek, JANOUŠEK Vladimír a ZBOŘIL František. Object Oriented Petri Nets - Modelling Techniques Case Study. International Journal of Simulation Systems, Science & Technology, roč. 10, č. 3, 2010, s. 32-44. ISSN 1473-8031. Detail

2009

  • KŘENA Bohuslav, LETKO Zdeněk, NIR-BUCHBINDER Yarden, TZOREF-BRILL Rachel, UR Shmuel a VOJNAR Tomáš. A Concurrency Testing Tool and its Plug-ins for Dynamic Analysis and Runtime Healing. FIT-TR-2009-01, Brno, 2009. Detail
  • KŘENA Bohuslav, LETKO Zdeněk, NIR-BUCHBINDER Yarden, TZOREF-BRILL Rachel, UR Shmuel a VOJNAR Tomáš. A Concurrency Testing Tool and its Plug-ins for Dynamic Analysis and Runtime Healing. In: Runtime Verification. Lecture Notes in Computer Science, Volume 5779/2009. Berlin: Springer Verlag, 2009, s. 101-114. ISBN 978-3-642-04693-3. Detail
  • ABDULLA Parosh A., HOLÍK Lukáš, KAATI Lisa a VOJNAR Tomáš. A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. Electronic Notes in Theoretical Computer Science, roč. 2009, č. 251, s. 27-48. ISSN 1571-0661. Detail
  • IOSIF Radu a ROGALEWICZ Adam. Automata-Based Termination Proofs. In: Implementation and Application of Automata. Lecture Notes in Computer Science, roč. 5642. Berlin: Springer Verlag, 2009, s. 165-177. ISBN 978-3-642-02978-3. Detail
  • BOZGA Marius, HABERMEHL Peter, IOSIF Radu, KONEČNÝ Filip a VOJNAR Tomáš. Automatic Verification of Integer Array Programs. In: Computer Aided Verification. Lecture Notes in Computer Science, roč. 5643. Berlin: Springer Verlag, 2009, s. 157-172. ISBN 978-3-642-02657-7. Detail
  • BOZGA Marius, HABERMEHL Peter, IOSIF Radu, KONEČNÝ Filip a VOJNAR Tomáš. Automatic Verification of Integer Array Programs. TR-2009-2, Grenoble: VERIMAG, 2009. Detail
  • ABDULLA Parosh A., BOUAJJANI Ahmed, HOLÍK Lukáš, KAATI Lisa a VOJNAR Tomáš. Composed Bisimulation for Tree Automata. International Journal of Foundations of Computer Science, roč. 20, č. 4, 2009, s. 685-700. ISSN 0129-0541. Detail
  • JANOUŠEK Vladimír a KIRONSKÝ Elöd. Interactive evolutionary modelling and simulation of discrete-event systems using prototypical objects. International Journal of Autonomic Computing, roč. 1, č. 2, 2009, s. 104-120. ISSN 1741-8569. Detail
  • ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang a VOJNAR Tomáš. Mediating for Reduction (On Minimizing Alternating Büchi Automata). Brno: Fakulta informačních technologií VUT v Brně, 2009. Detail
  • ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang a VOJNAR Tomáš. Mediating for Reduction (On Minimizing Alternating Büchi Automata). FIT-TR-2009-02, Brno, 2009. Detail
  • ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang a VOJNAR Tomáš. Zprostředkování pro redukci (Za minimalizací alternujících automatů). In: 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
  • MAZAL Zdeněk, KOČÍ Radek, JANOUŠEK Vladimír a ZBOŘIL František. Modelling intelligent agents for autonomic computing in the PNagent framework. International Journal of Autonomic Computing, roč. 1, č. 2, 2009, s. 121-139. ISSN 1741-8569. Detail
  • KOČÍ Radek a JANOUŠEK Vladimír. On the Dynamic Features of PNtalk. In: International Workshop on Petri Nets and Software Engineering 2009. Paříž: Université Pierre et Marie Curie, 2009, s. 189-206. Detail
  • JANOUŠEK Vladimír a KVĚTOŇOVÁ Šárka. On the Multilevel Petri Nets-Based Models in Project Engineering. In: International Workshop on Petri Nets and Software Engineering 2009. Paříž: Université Pierre et Marie Curie, 2009, s. 173-188. Detail
  • HOLÍK Lukáš a ŠIMÁČEK Jiří. Optimizing an LTS-Simulation Algorithm. FIT-TR-2009-03, Brno, 2009. Detail
  • HOLÍK Lukáš a ŠIMÁČEK Jiří. Optimizing an LTS-Simulation Algorithm. In: 5th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Znojmo: Fakulta informatiky MU, 2009, s. 93-101. ISBN 978-3-939897-15-6. Detail
  • DUDKA Vendula, VOJNAR Tomáš a KŘENA Bohuslav. Self-healing Assurance using Bounded Model Checking. In: Computer Aided Systems Theory. Las Palmas de Grand Canaria: Universidad de Las Palmas de Gran Canaria, 2009, s. 99-100. ISBN 978-84-691-8502-5. Detail
  • DUDKA Vendula, KŘENA Bohuslav a VOJNAR Tomáš. Self-healing Assurance using Bounded Model Checking. In: Computer Aided Systems Theory - EUROCAST 2009. Lecture Notes in Computer Science, roč. 5717. Berlin: Springer Verlag, 2009, s. 295-303. ISBN 978-3-642-04771-8. Detail
  • KOČÍ Radek a JANOUŠEK Vladimír. Simulation Based Design of Control Systems Using DEVS and Petri Nets. In: Computer Aided Systems Theory - EUROCAST 2009. Lecture Notes in Computer Science, Volume 5717. Berlin: Springer Verlag, 2009, s. 849-856. ISBN 978-3-642-04771-8. Detail
  • KOČÍ Radek a JANOUŠEK Vladimír. Towards Simulation-Based Design of the Software Systems. In: The Fourth International Conference on Software Engineering Advances. Los Alamitos: IEEE Computer Society, 2009, s. 452-457. ISBN 978-1-4244-4779-4. Detail

2008

  • HABERMEHL Peter, IOSIF Radu a VOJNAR Tomáš. A Logic of Singly Indexed Arrays. In: Logic for Programming, Artificial Intelligence and Reasoning. Lecture Notes in Computer Science, roč. 5330. Berlin: Springer Verlag, 2008, s. 558-573. ISBN 978-3-540-89438-4. Detail
  • HABERMEHL Peter, IOSIF Radu a VOJNAR Tomáš. A Logic of Singly Indexed Arrays. TR-2008-9, Grenoble: VERIMAG, 2008. Detail
  • ABDULLA Parosh A., HOLÍK Lukáš, KAATI Lisa a VOJNAR Tomáš. A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. FIT-TR-2008-005, Brno, 2008. Detail
  • ABDULLA Parosh A., HOLÍK Lukáš, KAATI Lisa a VOJNAR Tomáš. A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. In: 4th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Brno: Fakulta informatiky MU, 2008, s. 3-11. ISBN 978-80-7355-082-0. Detail
  • NOVOSAD Petr a ČEŠKA Milan. Algorithms for Computing Coverability Graphs for Continuous Petri Nets. In: Proceedings of 22th European Simulation and Modelling Conference ESM'2008. EUROSIS-ETI Publications. Le Havre: EUROSIM-FRANCOSIM-ARGESIM, 2008, s. 489-491. ISBN 978-90-77381-44-1. Detail
  • NOVOSAD Petr a ČEŠKA Milan. Algorithms for Computing Coverability Graphs for Hybrid Petri Nets. In: 4th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Brno: Masarykova universita, 2008, s. 177-183. ISBN 978-80-7355-082-0. Detail
  • LETKO Zdeněk. An Architecture for Self-Healing of Data Races and Atomicity Violations for Java. In: Proceedings of the 14th Conference STUDENT EEICT 2008. Volume 2. Brno: Vysoké učení technické v Brně, 2008, s. 256-258. ISBN 978-80-214-3615-2. Detail
  • BOUAJJANI Ahmed, HABERMEHL Peter, HOLÍK Lukáš, TOUILI Tayssir a VOJNAR Tomáš. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. In: Implementation and Application of Automata. Lecture Notes in Computer Science, roč. 5148. Berlin: Springer Verlag, 2008, s. 57-67. ISBN 978-3-540-70843-8. Detail
  • BOUAJJANI Ahmed, HABERMEHL Peter, HOLÍK Lukáš, TOUILI Tayssir a VOJNAR Tomáš. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. FIT-TR-2008-007, Brno: Fakulta informačních technologií VUT v Brně, 2008. Detail
  • LETKO Zdeněk, VOJNAR Tomáš a KŘENA Bohuslav. AtomRace: Data Race and Atomicity Violation Detector and Healer. In: PADTAD '08. Proceedings of the 6th workshop on Parallel and distributed systems. Seattle: Association for Computing Machinery, 2008, s. 1-10. ISBN 978-1-60558-052-4. Detail
  • VOJNAR Tomáš, ČEŠKA Milan, ROGALEWICZ Adam, ERLEBACH Pavel, HOLÍK Lukáš, BOUAJJANI Ahmed, HABERMEHL Peter, TOUILI Tayssir a MORO Pierre. Automatická verifikace programů s dynamickými datovými strukturami. Inovační podnikání & transfer technologií, roč. 2008, č. 1, s. 21-22. ISSN 1210-4612. Detail
  • DUDKA Vendula. Bounded Model Checking Using Java PathFinder. In: Proceedings of the 14th Conference STUDENT EEICT 2008. Volume 2. Brno: Vysoké učení technické v Brně, 2008, s. 247-249. ISBN 978-80-214-3615-2. Detail
  • ABDULLA Parosh A., BOUAJJANI Ahmed, HOLÍK Lukáš, KAATI Lisa a VOJNAR Tomáš. Composed Bisimulation for Tree Automata. FIT-TR-2008-004, Brno, 2008. Detail
  • ABDULLA Parosh A., BOUAJJANI Ahmed, HOLÍK Lukáš, KAATI Lisa a VOJNAR Tomáš. Composed Bisimulation for Tree Automata. In: Implementation and Application of Automata. Lecture Notes in Computer Science, roč. 5148. Berlin: Springer Verlag, 2008, s. 212-222. ISBN 978-3-540-70843-8. Detail
  • ABDULLA Parosh A., BOUAJJANI Ahmed, HOLÍK Lukáš, KAATI Lisa a VOJNAR Tomáš. Computing Simulations over Tree Automata (Efficient Techniques for Reducing Tree Automata). In: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, roč. 4963. Berlin: Springer Verlag, 2008, s. 93-108. ISBN 978-3-540-78799-0. Detail
  • ABDULLA Parosh A., BOUAJJANI Ahmed, HOLÍK Lukáš, KAATI Lisa a VOJNAR Tomáš. Computing Simulations over Tree Automata: Efficient Techniques for Reducing Tree Automata. FIT-TR-2008-001, Brno, 2008. Detail
  • MAZAL Zdeněk, JANOUŠEK Vladimír a KOČÍ Radek. Enhancing the PNtalk Language with Negative Predicates. In: MOSIS '08. Ostrava: MARQ, 2008, s. 28-34. ISBN 978-80-86840-40-6. Detail
  • POLÁŠEK Petr a JANOUŠEK Vladimír. Modeling and Simulation Management in Distributed Environment Using Web Services. In: Proceedings of the 14th International Congress of Cybernetics and Systems of WOCS. Wroclaw: Politechnika Wrocławska, 2008, s. 9. ISBN 978-83-7493-400-8. Detail
  • KOČÍ Radek, JANOUŠEK Vladimír a ZBOŘIL František. Object Oriented Petri Nets -- Modelling Techniques Case Study. In: Second UKSIM European Symposium on Computer Modeling and Simulation. Liverpool: IEEE Computer Society, 2008, s. 165-170. ISBN 978-0-7695-3325-4. Detail
  • JANOUŠEK Vladimír, KOČÍ Radek, MAZAL Zdeněk a ZBOŘIL František. PNagent: a Framework for Modelling BDI Agents using Object Oriented Petri Nets. In: Proceedings of 8th ISDA. Los Alamitos: IEEE Computer Society, 2008, s. 420-425. ISBN 978-0-7695-3382-7. Detail
  • HABERMEHL Peter a VOJNAR Tomáš, ed. Proceedings of 10th International Workshop on Verification of Infinite-State Systems - INFINITY'08. Toronto: Fakulta informačních technologií VUT v Brně, 2008. ISBN 978-80-214-3697-8. Detail
  • JANOUŠEK Vladimír a KIRONSKÝ Elöd. Reflective Framework for Interactive Modeling and Simulation of Intelligent Systems. In: Proceedings of Nineteenth International Conference on Systems Engineering 19-21 August 2008 Las Vegas, Nevada. Los Alamitos: IEEE Computer Society, 2008, s. 480-485. ISBN 978-0-7695-3331-5. Detail
  • KOČÍ Radek a JANOUŠEK Vladimír. System Design with Object Oriented Petri Nets Formalism. In: The Third International Conference on Software Engineering Advances Proceedings ICSEA 2008. Los Alamitos: IEEE Computer Society, 2008, s. 421-426. ISBN 978-0-7695-3372-8. Detail
  • JANOUŠEK Vladimír a KOČÍ Radek. The PNtalk/SmallDEVS Framework -- Meta-level Modeling Techniques. In: Proceedings of CSE 2008 International Scientific Conference on Computer Science and Engineering. Košice: elfa, s.r.o., TU v Košiciach, 2008, s. 16-23. ISBN 978-80-8086-092-9. Detail
  • SKLENÁŘ Jaroslav, CUTARAJ Valerie a ČEŠKA Milan. Using Integer Programming for Discrete Problem Optimization. In: The 2008 European Simulation and Modelling Conference. EUROSIS-ETI Publications. LE HAVRE: EUROSIM-FRANCOSIM-ARGESIM, 2008, s. 19-21. ISBN 978-90-77381-44-1. Detail
  • BOUAJJANI Ahmed, HABERMEHL Peter a VOJNAR Tomáš. Verification of parametric concurrent systems with prioritised FIFO resource management. Formal Methods in System Design, roč. 32, č. 2, 2008, s. 129-172. ISSN 0925-9856. Detail
  • HÝSEK Jiří. Visual design of SmallDEVS models using statecharts. In: Proceedings of ASIS 2008. Rožnov pod Radhoštěm: Grantová agentura České republiky, 2008, s. 6. ISBN 978-80-86840-42-0. Detail
  • HABERMEHL Peter, IOSIF Radu a VOJNAR Tomáš. What else is decidable about integer arrays?. In: Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science, roč. 4962. Berlin: Springer Verlag, 2008, s. 475-490. ISBN 978-3-540-78497-5. Detail
  • HABERMEHL Peter, IOSIF Radu a VOJNAR Tomáš. What else is decidable about integer arrays?. TR-2007-8, Grenoble: VERIMAG, 2008. Detail

2007

  • JANOUŠEK Vladimír, KIRONSKÝ Elöd a POLÁŠEK Petr. 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: Politechnika Wrocławska, 2007, s. 396-405. ISBN 978-83-7493-339-1. Detail
  • 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
  • JANOUŠEK Vladimír a KOČÍ Radek. Embedding Object-Oriented Petri Nets into a DEVS-based Simulation Framework. In: Proceedings of the 16th International Conference on System Science. volume 1. Wroclaw: Politechnika Wrocławska, 2007, s. 386-395. ISBN 978-83-7493-339-1. 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
  • KŘENA Bohuslav, LETKO Zdeněk, TZOREF-BRILL Rachel, UR Shmuel a VOJNAR Tomáš. 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, s. 54-64. ISBN 978-1-59593-734-6. Detail
  • ZBOŘIL František a KOČÍ Radek. Intention Structures Modelling Using Object Oriented Petri Nets. In: Proceedings of the 7th ISDA. Los Alamitos: IEEE Computer Society, 2007, s. 33-38. ISBN 0-7695-2976-3. Detail
  • KOČÍ Radek, MAZAL Zdeněk, ZBOŘIL František a JANOUŠEK Vladimír. Modeling Deliberative Agents Using Object Oriented Petri Nets. In: Proceedings of the 7th ISDA. Los Alamitos: IEEE Computer Society, 2007, s. 15-20. ISBN 0-7695-2976-3. Detail
  • ČEŠKA Milan, ERLEBACH Pavel a VOJNAR Tomáš. Pattern-based Verification for Trees. In: Computer Aided Systems Theory. Lecture Notes in Computer Science, roč. 4739. Berlin: Springer Verlag, 2007, s. 488-496. ISBN 978-3-540-75866-2. Detail
  • ČEŠKA Milan, ERLEBACH Pavel a VOJNAR Tomáš. Pattern-Based Verification for Trees. In: Computer Aided Systems Theory - EUROCAST 2007. Las Palmas de Grand Canaria: Universidad de Las Palmas de Gran Canaria, 2007, s. 181-182. ISBN 978-3-540-75866-2. Detail
  • HABERMEHL Peter, IOSIF Radu, ROGALEWICZ Adam a VOJNAR Tomáš. Proving Termination of Tree Manipulating Programs. In: Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, roč. 4762. Berlin: Springer Verlag, 2007, s. 145-161. ISBN 978-3-540-75595-1. Detail
  • JANOUŠEK Vladimír a KOČÍ Radek. 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, s. 9. ISBN 978-3-901608-32-2. Detail
  • VOJNAR Tomáš. Stromové automaty s omezeními v symbolické verifikaci programů manipulujících vyvážené stromy. Současné trendy teoretické informatiky. ITI Series 2007-347. Praha, 2007. Detail
  • DUDKA Vendula, KŘENA Bohuslav a VOJNAR Tomáš. 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, s. 67-73. ISBN 978-80-7355-077-6. Detail
Produkty

2009

  • Analyzátor CDC asynchronních komponent, software, 2009
    Autoři: Smrčka Aleš Detail
  • FLATA, software, 2009
    Autoři: Konečný Filip, Vojnar Tomáš, Bozga Marius, Iosif Radu Detail
  • Nástroj pro výpočet simulací, software, 2009
    Autoři: Holík Lukáš, Šimáček Jiří, Vojnar Tomáš Detail

2008

  • MUSE - model checking s využitím symbolického provádění, software, 2008
    Autoři: Křena Bohuslav, Braione Pietro, Denaro Giovanni, Pezze Mauro Detail
  • Nástroj pro detekci a opravu chyb v atomicitě programů, software, 2008
    Autoři: Letko Zdeněk, Vojnar Tomáš, Křena Bohuslav Detail
  • PNtalk, software, 2008
    Autoři: Kočí Radek Detail

2007

  • Nástroj pro detekci a opravu časově závislých chyb v Javě, software, 2007
    Autoři: Letko Zdeněk, Vojnar Tomáš, Křena Bohuslav Detail
  • SmallDEVS-07, software, 2007
    Autoři: Janoušek Vladimír, Kironský Elöd Detail
Nahoru