Detail projektu

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

Období řešení: 1. 1. 2004 – 31. 12. 2006

Typ projektu: grant

Kód: GA102/04/0780

Agentura: Grantová agentura České republiky

Program: Standardní projekty

Název anglicky
Automated methods and tools supporting development of reliable parallel and distributed systems
Typ
grant
Klíčová slova

Modeling, simulation, verification, prototyping, parallel, distrubuted

Abstrakt

Cílem projektu je rozvoj stávajících a návrh nových automatizovaných metod
a nástrojů pro modelování a prototypování moderních paralelních a distribuovaných
systémů a pro ověřování korektnosti těchto systémů a nebo jejich částí na úrovni
specializovaných abstraktních modelů i prototypů. Řešení vychází převážně
z původního matematického modelu objektově orientovaných Petriho sítí, který byl
vytvořen řešiteli na FIT VUT v Brně a který spojuje výhody vysokoúrovňových
Petriho sítí s výhodami objektově orientovaných návrhových technologií. Pro
potřeby ověřování korektnosti uvažovaných systémů budou rozvíjeny metody
efektivní simulace a formální analýzy a verifikace, včetně možnosti paralelního
či distribuovaného řešení. Projekt přinese metodologii a příslušné počítačové
nástroje pro podporu modelování a prototypování paralelních a distribuovaných
systémů s využitím vybraných metod formální analýzy a verifikace. Vyvinuté
počítačové nástroje budou integrovány ve formě otevřeného prostředí, využitelného
jak pro podporu navazujícího výzkumu, tak v reálných aplikacích.

Řešitelé
Češka Milan, prof. RNDr., CSc. – hlavní řešitel
Haša Luděk, Ing.
Janoušek Vladimír, doc. Ing., Ph.D. (UITS)
Kočí Radek, Ing., Ph.D. (UITS)
Křena Bohuslav, Ing., Ph.D. (UITS)
Rábová Zdeňka, doc. Ing., CSc.
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Publikace

2008

  • 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

2007

  • 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
  • ROGALEWICZ, A. Verification of Programs with Complex Data Structures. Brno: 2007. 122 p. ISBN: 978-80-214-3548-3. Detail
  • SMRČKA, A.; ŘEHÁK, V.; VOJNAR, T.; ŠAFRÁNEK, D.; MATOUŠEK, P.; ŘEHÁK, Z. Verifying VHDL Design with Multiple Clocks in SMV. In Formal Methods: Applications and Technology. Lecture Notes in Computer Science. Lecture Notes in Computer Science 4346. Bonn: Springer Verlag, 2007. p. 148-164. ISBN: 978-3-540-70951-0. ISSN: 0302-9743. 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
  • ČEŠKA, M.; JANOUŠEK, V.; KOČÍ, R.; KŘENA, B.; VOJNAR, T. PNtalk: State of the Art. Proceedings of the Fourth International Workshop on Modelling of Objects, Components, and Agents. Hamburg: 2006. p. 301-307. 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
  • IOSIF, R.; HABERMEHL, P.; VOJNAR, T.; BOUAJJANI, A.; BOZGA, M.; MORO, P. Programs with Lists are Counter Automata. Computer Aided Verification. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2006. p. 517-531. ISBN: 978-3-540-37406-0. Detail
  • JANOUŠEK, V. On the Prototype-Based Object Orientation in Modeling and Simulation. Proceedings of of Advanced Simulation of Systems 2006. Ostrava: 2006. p. 1-6. ISBN: 80-86840-26-3. Detail
  • JANOUŠEK, V.; KIRONSKÝ, E. Exploratory Modeling with SmallDEVS. Proc. of ESM 2006. Ghent: EUROSIS, 2006. p. 122-126. ISBN: 90-77381-30-9. Detail
  • JANOUŠEK, V.; KIRONSKÝ, E. SmallDEVS, an Interactive Modeling and Simulation Tool for Smalltalk. Proc. of MOSIS'06. Ostrava: 2006. p. 91-98. ISBN: 80-86840-21-2. Detail
  • JANOUŠEK, V.; KOČÍ, R. Formální modely a simulace ve vývoji softwarových systémů. Proceedings of ASIS'06. Ostrava: MARQ, 2006. s. 164-169. ISBN: 8086840263. Detail
  • JANOUŠEK, V.; POLÁŠEK, P.; SLAVÍČEK, P. Metajazyk pro popis DEVS formalismu. NETSS 2006. Ostrava: MARQ, 2006. s. 43-48. ISBN: 80-86840-06-9. Detail
  • JANOUŠEK, V.; POLÁŠEK, P.; SLAVÍČEK, P. Towards DEVS Meta Language. ISC 2006 Proceedings. Zwijnaarde: 2006. p. 69-73. ISBN: 90-77381-26-0. Detail
  • KOČÍ, R.; TURAKHODJAEVA, N. Modeling Workflow Using Object Oriented Petri Nets. Proceedings of ASIS'06. Ostrava: 2006. p. 127-132. ISBN: 8086840263. Detail
  • KŘENA, B. Computer Go as a Verification Case Study. Proceedings of XXVIIIth International Autumn Colloquium ASIS 2006: Advanced Simulation of Systems. Ostrava: 2006. p. 95-100. ISBN: 80-86840-26-3. Detail
  • SMRČKA, A.; ŘEHÁK, V.; VOJNAR, T.; ŠAFRÁNEK, D.; MATOUŠEK, P.; ŘEHÁK, Z. Verifying VHDL Design with Multiple Clocks in SMV. Proceedings of FMICS 2006. Bonn: 2006. p. 140-155. 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
  • ČEŠKA, M.; KŘENA, B.; VOJNAR, T. Parallel State Space Generation and Exploration on Shared-Memory Architectures. EUROCAST2005: Cast and Tools for Robotics, Vehicular and Communication Systems. Las Palmas de Gran Canaria: The Universidad de Las Palmas de Gran Canaria, 2005. p. 161-164. ISBN: 84-689-0432-5. Detail
  • ČEŠKA, M.; TURAKHODJAEVA, N. Verification of Worklow Management Systems described by Object-Oriented Petri Nets. Proceedings of XXVIIth International Autumn Colloquium ASIS 2005. Ostrava: 2005. p. 189-198. ISBN: 80-86840-16-6. 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
  • JANOUŠEK, V.; KOČÍ, R. PNtalk Project: Current Research Direction. Simulation Almanac 2005. Praha: Faculty of Electrical Engineering, Czech Technical University, 2005. p. 50-62. ISBN: 80-01-03322-8. Detail
  • JANOUŠEK, V.; KOČÍ, R. Towards Model-Based Design with PNtalk. Proceedings of the International Workshop MOSMIC'2005. Žilina: Faculty of management science and Informatics of Zilina University, 2005. p. 59-66. ISBN: 80-8070-468-6. Detail
  • JANOUŠEK, V.; SLAVÍČEK, P. Concept for the parallel road-traffic simulation. Proceedings of MOSIS'05. Ostrava: 2005. p. 123-128. ISBN: 80-86840-10-7. Detail
  • KOČÍ, R.; TURAKHODJAEVA, N. Workflow modeling with Petri nets in Workflow Management Systems. Proceedings of MOSIS'05. Ostrava: 2005. p. 120-127. ISBN: 80-86840-10-7. 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
  • MAREK, V. State-space Exploration of Petri Nets. Proceedings of 39th International Conference MOSIS '05. Ostrava: 2005. p. 114-119. ISBN: 80-86840-10-7. Detail
  • MATOUŠEK, P.; SMRČKA, A.; VOJNAR, T. High-Level Modelling, Analysis, and Verification on FPGA-Based Hardware Design. Correct Hardware Design and Verification Methods. Lecture Notes in Computer Science. Lecture Notes in Computer Science 3725/2005. Berlin: Springer Verlag, 2005. p. 371-375. ISBN: 978-3-540-29105-3. ISSN: 0302-9743. 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
  • SCHWARZ, I.; ČEŠKA, M.; JANOUŠEK, V. Towards an Implementation of Distributed PNtalk. Proceedings of 39th Spring International Conference MOSIS'05 Modelling and Simulation of Systems. Ostrava: 2005. p. 166-173. ISBN: 80-86840-10-7. Detail
  • SMRČKA, A. Abstract Model Verification of the Lookup Processor. In Proceedings of MOSIS'05. Ostrava: 2005. p. 138-145. ISBN: 80-86840-10-7. Detail
  • SMRČKA, A. Towards Hardware Verification. In Proceedings of the 11th Conference Student EEICT 2005. Volume 3. Brno: Faculty of Information Technology BUT, 2005. p. 668-672. ISBN: 978-80-214-2890-4. 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
  • HAŠA, L.; ČEŠKA, M. Improvements in Model Checking for Object-Oriented Petri Nets. 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. p. 269-274. ISBN: 980-6560-19-1. Detail
  • HRUBÝ, M.; JANOUŠEK, V.; KOČÍ, R. Vývoj pokročilých metod modelování a protypování komplikovaných systémů. NETSS2004. Ostrava: MARQ, 2004. s. 103-108. ISBN: 80-85988-92-5. 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
  • KOČÍ, R. Open Implementation of the Simulation Framework. Proceedings of 38th International Conference MOSIS'04. Ostrava: 2004. p. 73-80. ISBN: 80-85988-98-4. Detail
  • MAREK, V. State-space Model Based on Graph Rewriting. Proceedings of 7th International Conference ISIM '04. Ostrava: 2004. p. 133-140. ISBN: 80-85988-99-2. 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
Nahoru