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: Standardní projekty
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 (http://perchta.fit.vutbr.cz/intelligentsystems/103)]
Řešitelé
Češka Milan, prof. RNDr., CSc.
– hlavní řešitel
Cerhák Michal, Ing.
Cerhák Michal, Ing.
Erlebach Pavel, Ing., Ph.D.
Erlebach Pavel, Ing., Ph.D.
Holík Lukáš, doc. Mgr., Ph.D. (UITS)
Holík Lukáš, doc. Mgr., Ph.D. (UITS)
Janoušek Vladimír, doc. Ing., Ph.D. (UITS)
Janoušek Vladimír, doc. Ing., Ph.D. (UITS)
Kironský Elöd, Ing.
Kironský Elöd, Ing.
Kočí Radek, Ing., Ph.D. (UITS)
Kočí Radek, Ing., Ph.D. (UITS)
Křena Bohuslav, Ing., Ph.D. (UITS)
Křena Bohuslav, Ing., Ph.D. (UITS)
Polášek Petr, Ing., Ph.D.
Polášek Petr, Ing., Ph.D.
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Smrčka Aleš, Ing., Ph.D. (UITS)
Smrčka Aleš, Ing., Ph.D. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Cerhák Michal, Ing.
Cerhák Michal, Ing.
Erlebach Pavel, Ing., Ph.D.
Erlebach Pavel, Ing., Ph.D.
Holík Lukáš, doc. Mgr., Ph.D. (UITS)
Holík Lukáš, doc. Mgr., Ph.D. (UITS)
Janoušek Vladimír, doc. Ing., Ph.D. (UITS)
Janoušek Vladimír, doc. Ing., Ph.D. (UITS)
Kironský Elöd, Ing.
Kironský Elöd, Ing.
Kočí Radek, Ing., Ph.D. (UITS)
Kočí Radek, Ing., Ph.D. (UITS)
Křena Bohuslav, Ing., Ph.D. (UITS)
Křena Bohuslav, Ing., Ph.D. (UITS)
Polášek Petr, Ing., Ph.D.
Polášek Petr, Ing., Ph.D.
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Smrčka Aleš, Ing., Ph.D. (UITS)
Smrčka Aleš, Ing., Ph.D. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Publikace
2010
- 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 - 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
2009
- ABDULLA, P.; HOLÍK, L.; CHEN, Y.; VOJNAR, T. Mediating for Reduction (On Minimizing Alternating Büchi Automata). Brno: Faculty of Information Technology BUT, 2009.
p. 0-0. 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 - 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 - 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 - HOLÍK, L.; ŠIMÁČEK, J. Optimizing an LTS-Simulation Algorithm. FIT-TR-2009-03, Brno: 2009.
p. 0-0. 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 - HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; CHEN, Y. Mediating for Reduction (On Minimizing Alternating Büchi Automata). FIT-TR-2009-02, Brno: 2009.
p. 0-0. Detail - HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; CHEN, Y. Mediating for Reduction (On Minimizing Alternating Büchi Automata). 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 - 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.; 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 - IOSIF, R.; KONEČNÝ, F.; VOJNAR, T.; HABERMEHL, P.; BOZGA, M. Automatic Verification of Integer Array Programs. TR-2009-2, Grenoble: VERIMAG, 2009.
p. 0-0. 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 - 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 - 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 - 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 - 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 - 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 - 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 - LETKO, Z.; VOJNAR, T.; KŘENA, B.; NIR-BUCHBINDER, Y.; TZOREF-BRILL, R.; UR, S. A Concurrency Testing Tool and its Plug-ins for Dynamic Analysis and Runtime Healing. FIT-TR-2009-01, Brno: 2009.
p. 0-0. 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
2008
- 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 - HABERMEHL, P.; IOSIF, R.; VOJNAR, T. A Logic of Singly Indexed Arrays. TR-2008-9, Grenoble: VERIMAG, 2008.
p. 0-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 - HABERMEHL, P.; IOSIF, R.; VOJNAR, T. What else is decidable about integer arrays?. TR-2007-8, Grenoble: VERIMAG, 2008.
p. 0-0. Detail - HABERMEHL, P.; VOJNAR, T. Proceedings of 10th International Workshop on Verification of Infinite-State Systems - INFINITY'08. Toronto: Faculty of Information Technology BUT, 2008.
p. 0-0. ISBN: 978-80-214-3697-8. Detail - HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; BOUAJJANI, A.; KAATI, L. Composed Bisimulation for Tree Automata. FIT-TR-2008-004, Brno: 2008.
p. 0-0. 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.; 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 - 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.
p. 0-0. 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 - 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.
p. 0-0. 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.
p. 0-0. 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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
2007
- DUDKA, V.; KŘENA, B.; VOJNAR, T. Using JavaPathFinder for Self-healing Assurance. 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 - ERLEBACH, P.; ČEŠKA, M.; VOJNAR, T. Pattern-Based Verification for Trees. 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 - 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 - ERLEBACH, P.; VOJNAR, T.; ČEŠKA, M. Pattern-based Verification for Trees. Computer Aided Systems Theory. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2007.
p. 488-496. ISBN: 978-3-540-75866-2. Detail - HABERMEHL, P.; IOSIF, R.; ROGALEWICZ, A.; VOJNAR, T. Proving Termination of Tree Manipulating Programs. Automated Technology for Verification and Analysis. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2007.
p. 145-161. ISBN: 978-3-540-75595-1. Detail - JANOUŠEK, V.; KIRONSKÝ, E.; POLÁŠEK, P. An Architecture for Simulation-Based Evolutionary Design of Systems. 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 - JANOUŠEK, V.; KOČÍ, R. Embedding Object-Oriented Petri Nets into a DEVS-based Simulation Framework. 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. 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 - KOČÍ, R.; MAZAL, Z.; ZBOŘIL, F.; JANOUŠEK, V. Modeling Deliberative Agents Using Object Oriented Petri Nets. Proceedings of the 7th ISDA. Los Alamitos: IEEE Computer Society, 2007.
p. 15-20. ISBN: 0-7695-2976-3. Detail - KŘENA, B.; LETKO, Z.; TZOREF-BRILL, R.; UR, S.; VOJNAR, T. Healing Data Races On-The-Fly. 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 - 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
- VOJNAR, T. 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.
s. 38-39. Detail - ZBOŘIL, F.; KOČÍ, R. Intention Structures Modelling Using Object Oriented Petri Nets. Proceedings of the 7th ISDA. Los Alamitos: IEEE Computer Society, 2007.
p. 33-38. ISBN: 0-7695-2976-3. Detail