Project Details

Automatizované metody a nástroje pro vývoj spolehlivých paralelních a distribuovaných systémů

Project Period: 1. 1. 2004 - 31. 12. 2006

Project Type: grant

Code: GA102/04/0780

Agency: Czech Science Foundation

Program:

English title
Automated methods and tools supporting development of reliable parallel and distributed systems
Type
grant
Keywords

Modeling, simulation, verification, prototyping, parallel, distrubuted

Abstract

The goal of the project is to improve the existing and to propose new automated methods and tools for modelling and prototyping modern concurrent and distributed systems and for checking correctness of such systems (or their key parts) at the level of specialized abstract models as well as prototypes. The proposed approach builds to a large degree upon the original formal model of object-oriented Petri nets that has been proposed by the project team members at the Faculty of Information Technology of the Brno University of Technology and that combines advantages of high-level Petri nets and object-oriented design technologies. The project will bring in a methodology and computer-aided tools for modelling and prototyping concurrent and distributed computerized systems with various methods applicable for validating correctness of these systems. For the needs of the correctness validation,methods of efficient simulation and formal analysis and verification (including the possibility of their parallel or distributed solution) will be being developed. The tools resulting from the project will be integrated in an open and flexible environment useful both as a support for future research as well as for real applications.

Team members
Češka Milan, prof. RNDr., CSc. (UITS FIT VUT) , research leader
Haša Luděk, Ing. (UITS FIT VUT) , team leader
Janoušek Vladimír, doc. Ing., Ph.D. (UITS FIT VUT) , team leader
Kočí Radek, Ing., Ph.D. (UITS FIT VUT) , team leader
Křena Bohuslav, Ing., Ph.D. (UITS FIT VUT) , team leader
Rábová Zdeňka, doc. Ing., CSc. (UITS FIT VUT) , team leader
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT) , team leader
Publications

2008

  • VOJNAR Tomáš, ČEŠKA Milan, ROGALEWICZ Adam, ERLEBACH Pavel, HOLÍK Lukáš, BOUAJJANI Ahmed, HABERMEHL Peter, TOUILI Tayssir and MORO Pierre. Automatická verifikace programů s dynamickými datovými strukturami. Inovační podnikání & transfer technologií, vol. 2008, no. 1, pp. 21-22. ISSN 1210-4612. Detail

2007

  • VOJNAR Tomáš. Cut-offs and Automata in Formal Verification of Infinite-State Systems. FIT Monograph 1. Brno: Faculty of Information Technology BUT, 2007. ISBN 978-80-214-3547-6. Detail
  • ČEŠKA Milan, ERLEBACH Pavel and VOJNAR Tomáš. Pattern-Based Verification for Trees. In: Computer Aided Systems Theory - EUROCAST 2007. Las Palmas de Grand Canaria: The Universidad de Las Palmas de Gran Canaria, 2007, pp. 181-182. ISBN 978-3-540-75866-2. Detail
  • ROGALEWICZ Adam. Verification of Programs with Complex Data Structures. Brno, 2007. ISBN 978-80-214-3548-3. Detail
  • SMRČKA Aleš, ŘEHÁK Vojtěch, VOJNAR Tomáš, ŠAFRÁNEK David, MATOUŠEK Petr and ŘEHÁK Zdeněk. Verifying VHDL Design with Multiple Clocks in SMV. In: Formal Methods: Applications and Technology. Lecture Notes in Computer Science, vol. 4346. Bonn: Springer Verlag, 2007, pp. 148-164. ISSN 0302-9743. Detail

2006

  • BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam and VOJNAR Tomáš. Abstract Regular Tree Model Checking. Electronic Notes in Theoretical Computer Science, vol. 149, no. 1, 2006, pp. 37-48. ISSN 1571-0661. Detail
  • BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam and VOJNAR Tomáš. Abstract Regular Tree Model Checking of Complex Dynamic Data Structures. In: Static Analysis. Lecture Notes in Computer Science, vol. 4134. Berlin: Springer Verlag, 2006, pp. 52-70. ISBN 978-3-540-37756-6. Detail
  • HABERMEHL Peter, IOSIF Radu and 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, vol. 3920. Berlin: Springer Verlag, 2006, pp. 350-364. ISBN 978-3-540-33056-1. Detail
  • KŘENA Bohuslav. Computer Go as a Verification Case Study. In: Proceedings of XXVIIIth International Autumn Colloquium ASIS 2006: Advanced Simulation of Systems. Ostrava, 2006, pp. 95-100. ISBN 80-86840-26-3. Detail
  • JANOUŠEK Vladimír and KIRONSKÝ Elöd. Exploratory Modeling with SmallDEVS. In: Proc. of ESM 2006. Ghent: EUROSIS, 2006, pp. 122-126. ISBN 90-77381-30-9. Detail
  • JANOUŠEK Vladimír and KOČÍ Radek. Formální modely a simulace ve vývoji softwarových systémů. In: Proceedings of ASIS'06. Ostrava, 2006, pp. 164-169. ISBN 8086840263. Detail
  • JANOUŠEK Vladimír, POLÁŠEK Petr and SLAVÍČEK Pavel. Metajazyk pro popis DEVS formalismu. In: NETSS 2006. Ostrava, 2006, pp. 43-48. ISBN 80-86840-06-9. Detail
  • KOČÍ Radek and TURAKHODJAEVA Nasibakhon. Modeling Workflow Using Object Oriented Petri Nets. In: Proceedings of ASIS'06. Ostrava, 2006, pp. 127-132. ISBN 8086840263. Detail
  • JANOUŠEK Vladimír. On the Prototype-Based Object Orientation in Modeling and Simulation. In: Proceedings of of Advanced Simulation of Systems 2006. Ostrava, 2006, p. 6. ISBN 80-86840-26-3. Detail
  • ČEŠKA Milan, ERLEBACH Pavel and VOJNAR Tomáš. Pattern-Based Verification of Programs with Extended Linear Linked Data Structures. Electronic Notes in Theoretical Computer Science, vol. 2006, no. 145, pp. 113-130. ISSN 1571-0661. Detail
  • ČEŠKA Milan, JANOUŠEK Vladimír, KOČÍ Radek, KŘENA Bohuslav and VOJNAR Tomáš. PNtalk: State of the Art. In: Proceedings of the Fourth International Workshop on Modelling of Objects, Components, and Agents. Hamburg, 2006, pp. 301-307. Detail
  • BOUAJJANI Ahmed, BOZGA Marius, HABERMEHL Peter, IOSIF Radu, MORO Pierre and VOJNAR Tomáš. Programs with Lists are Counter Automata. In: Computer Aided Verification. Lecture Notes in Computer Science, vol. 4144. Berlin: Springer Verlag, 2006, pp. 517-531. ISBN 978-3-540-37406-0. Detail
  • JANOUŠEK Vladimír and KIRONSKÝ Elöd. SmallDEVS, an Interactive Modeling and Simulation Tool for Smalltalk. In: Proc. of MOSIS'06. Ostrava, 2006, pp. 91-98. ISBN 80-86840-21-2. Detail
  • JANOUŠEK Vladimír, POLÁŠEK Petr and SLAVÍČEK Pavel. Towards DEVS Meta Language. In: ISC 2006 Proceedings. Zwijnaarde, 2006, pp. 69-73. ISBN 90-77381-26-0. Detail
  • SMRČKA Aleš, ŘEHÁK Vojtěch, VOJNAR Tomáš, ŠAFRÁNEK David, MATOUŠEK Petr and ŘEHÁK Zdeněk. Verifying VHDL Design with Multiple Clocks in SMV. In: Proceedings of FMICS 2006. Bonn, 2006, pp. 140-155. Detail

2005

  • SMRČKA Aleš. Abstract Model Verification of the Lookup Processor. In: Proceedings of MOSIS'05. Ostrava, 2005, pp. 138-145. ISBN 80-86840-10-7. Detail
  • BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam and 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, pp. 15-24. ISSN 0909-3206. Detail
  • HABERMEHL Peter, IOSIF Radu and VOJNAR Tomáš. Automata-based Verification of Programs with Tree Updates. Verimag Technical Report number TR-2005-16, Grenoble: VERIMAG, 2005. Detail
  • ERLEBACH Pavel and 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, 2005, pp. 219-226. ISBN 80-86840-09-3. Detail
  • JANOUŠEK Vladimír and SLAVÍČEK Pavel. Concept for the parallel road-traffic simulation. In: Proceedings of MOSIS'05. Ostrava, 2005, pp. 123-128. ISBN 80-86840-10-7. Detail
  • ERLEBACH Pavel. Experience from Verifying in TVLA. In: EEICT'05. volume 3. Brno: Faculty of Electrical Engineering and Communication BUT, 2005, pp. 648-652. ISBN 80-214-2890-2. Detail
  • MATOUŠEK Petr, SMRČKA Aleš and VOJNAR Tomáš. High-Level Modelling, Analysis, and Verification on FPGA-Based Hardware Design. In: Correct Hardware Design and Verification Methods. Lecture Notes in Computer Science 3725/2005, vol. 2005. Berlin: Springer Verlag, 2005, pp. 371-375. ISBN 978-3-540-29105-3. ISSN 0302-9743. Detail
  • ČEŠKA Milan, KŘENA Bohuslav and VOJNAR Tomáš. Parallel State Space Generation and Exploration on Shared-Memory Architectures. In: EUROCAST2005: Cast and Tools for Robotics, Vehicular and Communication Systems. Las Palmas de Gran Canaria: The Universidad de Las Palmas de Gran Canaria, 2005, pp. 161-164. ISBN 84-689-0432-5. Detail
  • ČEŠKA Milan, KŘENA Bohuslav and VOJNAR Tomáš. Parallel State Space Generation and Exploration on Shared-Memory Architectures. In: Computer Aided Systems Theory - EUROCAST 2005. Lecture Notes in Computer Science, vol. 3643. Berlin: Springer Verlag, 2005, pp. 275-280. ISBN 978-3-540-29002-5. Detail
  • ČEŠKA Milan, ERLEBACH Pavel and 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, pp. 101-117. Detail
  • JANOUŠEK Vladimír and KOČÍ Radek. PNtalk Project: Current Research Direction. In: Simulation Almanac 2005. Praha: Faculty of Electrical Engineering, Czech Technical University, 2005, pp. 50-62. ISBN 80-01-03322-8. Detail
  • HABERMEHL Peter and VOJNAR Tomáš. Regular Model Checking Using Inference of Regular Languages. Electronic Notes in Theoretical Computer Science, vol. 138, no. 3, 2005, pp. 21-36. ISSN 1571-0661. Detail
  • MAREK Vladimír. State-space Exploration of Petri Nets. In: Proceedings of 39th International Conference MOSIS '05. Ostrava, 2005, pp. 114-119. ISBN 80-86840-10-7. 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: Faculty of Informatics MU, 2005, pp. 145-154. Detail
  • SCHWARZ Ivan, ČEŠKA Milan and JANOUŠEK Vladimír. Towards an Implementation of Distributed PNtalk. In: Proceedings of 39th Spring International Conference MOSIS'05 Modelling and Simulation of Systems. Ostrava, 2005, pp. 166-173. ISBN 80-86840-10-7. Detail
  • ROGALEWICZ Adam. Towards Applying Mona in Abstract Regular Tree Model Checking. In: Proceedings of the 11th Conference Student EEICT 2005. Volume 3. Brno: Faculty of Information Technology BUT, 2005, pp. 663-667. ISBN 80-214-2890-2. Detail
  • SMRČKA Aleš. Towards Hardware Verification. In: Proceedings of the 11th Conference Student EEICT 2005. Volume 3. Brno: Faculty of Information Technology BUT, 2005, pp. 668-672. ISBN 978-80-214-2890-4. Detail
  • JANOUŠEK Vladimír and KOČÍ Radek. Towards Model-Based Design with PNtalk. In: Proceedings of the International Workshop MOSMIC'2005. Žilina: Faculty of management science and Informatics of Zilina University, 2005, pp. 59-66. ISBN 80-8070-468-6. Detail
  • ČEŠKA Milan and TURAKHODJAEVA Nasibakhon. Verification of Worklow Management Systems described by Object-Oriented Petri Nets. In: Proceedings of XXVIIth International Autumn Colloquium ASIS 2005. Ostrava, 2005, pp. 189-198. ISBN 80-86840-16-6. Detail
  • BOUAJJANI Ahmed, HABERMEHL Peter, MORO Pierre and 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, vol. 3440. Berlin: Springer Verlag, 2005, pp. 13-29. ISBN 978-3-540-25333-4. Detail
  • KOČÍ Radek and TURAKHODJAEVA Nasibakhon. Workflow modeling with Petri nets in Workflow Management Systems. In: Proceedings of MOSIS'05. Ostrava, 2005, pp. 120-127. ISBN 80-86840-10-7. Detail

2004

  • BOUAJJANI Ahmed, HABERMEHL Peter and VOJNAR Tomáš. Abstract Regular Model Checking. Lecture Notes in Computer Science, vol. 2004, no. 3114, pp. 372-386. ISSN 0302-9743. Detail
  • ČEŠKA Milan and HAŠA Luděk. Improvements in Model Checking for Object-Oriented Petri Nets. In: Proceedings of the ISAS CITSA 2004, Volume III, Communications, Information and Control Systems, Technologies and Applications. Orlando: The International Institute of Informatics and Systemics, 2004, pp. 269-274. ISBN 980-6560-19-1. Detail
  • KOČÍ Radek. Open Implementation of the Simulation Framework. In: Proceedings of 38th International Conference MOSIS'04. Ostrava, 2004, pp. 73-80. ISBN 80-85988-98-4. Detail
  • HABERMEHL Peter and 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, pp. 61-71. Detail
  • MAREK Vladimír. State-space Model Based on Graph Rewriting. In: Proceedings of 7th International Conference ISIM '04. Ostrava, 2004, pp. 133-140. ISBN 80-85988-99-2. Detail
  • JANOUŠEK Vladimír and KOČÍ Radek. Towards an Open Implementation of the PNtalk System. In: 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, pp. 31-36. ISBN 3-901608-28-1. Detail
  • ROGALEWICZ Adam and VOJNAR Tomáš. Tree Automata In Modelling And Verification Of Concurrent Programs. In: Proceedings of ASIS 2004. Ostrava, 2004, pp. 197-202. ISBN 80-86840-03-4. Detail
  • HRUBÝ Martin, JANOUŠEK Vladimír and KOČÍ Radek. Vývoj pokročilých metod modelování a protypování komplikovaných systémů. In: NETSS2004. Ostrava, 2004, pp. 103-108. ISBN 80-85988-92-5. Detail
Back to top