Project Details

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

Project Period: 1. 1. 2007 – 31. 12. 2009

Project Type: grant

Code: GA102/07/0322

Agency: Czech Science Foundation

Program: Standardní projekty

English title
Advanced Formal Approaches in the Design and Verification of Computer-Based Systems
Type
grant
Keywords

formal models, simulation verification, formal verification, model checking

Abstract

High-level design and formal verification are promising approaches for improving
reliability and safety of computer systems. This project is proposed by the
highly experienced team with the expressive results and the international
cooperation with the prestigious research teams. The project aims to explore and
use advanced formal approaches from the fields like system theory, logics,
theoretical computer science, and artificial intelligence in the area of the
high-level design and formal verification. We believe that these approaches can
significantly improve the verification abilities, especially in the cases on
which the brute-force approach does not succeed. The proposed research project
covers complementary methods, i.e., the model-driven design, the simulation-based
verification, and the model checking of finite-state as well as infinite-state
systems. The research should result in developing new approaches and methods with
unique properties. These methods will be validated by the prototype
implementation and will be evaluated by suitable case studies.

Team members
Češka Milan, prof. RNDr., CSc. – research leader
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. (DITS)
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Janoušek Vladimír, doc. Ing., Ph.D. (DITS)
Janoušek Vladimír, doc. Ing., Ph.D. (DITS)
Kironský Elöd, Ing.
Kironský Elöd, Ing.
Kočí Radek, Ing., Ph.D. (DITS)
Kočí Radek, Ing., Ph.D. (DITS)
Křena Bohuslav, Ing., Ph.D. (DITS)
Křena Bohuslav, Ing., Ph.D. (DITS)
Polášek Petr, Ing., Ph.D.
Polášek Petr, Ing., Ph.D.
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS)
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS)
Smrčka Aleš, Ing., Ph.D. (DITS)
Smrčka Aleš, Ing., Ph.D. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Publications

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
Back to top