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:

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. (UITS FIT VUT) , hlavní řešitel
Haša Luděk, Ing. (UITS FIT VUT) , spoluřešitel
Janoušek Vladimír, doc. Ing., Ph.D. (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
Rábová Zdeňka, doc. Ing., CSc. (UITS FIT VUT) , spoluřešitel
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT) , spoluřešitel
Publikace

2008

  • 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

2007

  • 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
  • Č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
  • 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 a ŘEHÁK Zdeněk. Verifying VHDL Design with Multiple Clocks in SMV. In: Formal Methods: Applications and Technology. Lecture Notes in Computer Science, roč. 4346. Bonn: Springer Verlag, 2007, s. 148-164. ISSN 0302-9743. Detail

2006

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

2005

  • SMRČKA Aleš. Abstract Model Verification of the Lookup Processor. In: Proceedings of MOSIS'05. Ostrava: MARQ, 2005, s. 138-145. ISBN 80-86840-10-7. Detail
  • BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam a 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, s. 15-24. ISSN 0909-3206. Detail
  • HABERMEHL Peter, IOSIF Radu a VOJNAR Tomáš. Automata-based Verification of Programs with Tree Updates. Verimag Technical Report number TR-2005-16, Grenoble: VERIMAG, 2005. Detail
  • ERLEBACH Pavel a 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: MARQ, 2005, s. 219-226. ISBN 80-86840-09-3. Detail
  • JANOUŠEK Vladimír a SLAVÍČEK Pavel. Concept for the parallel road-traffic simulation. In: Proceedings of MOSIS'05. Ostrava: MARQ, 2005, s. 123-128. ISBN 80-86840-10-7. Detail
  • ERLEBACH Pavel. Experience from Verifying in TVLA. In: EEICT'05. volume 3. Brno: Fakulta elektrotechniky a komunikačních technologií VUT v Brně, 2005, s. 648-652. ISBN 80-214-2890-2. Detail
  • MATOUŠEK Petr, SMRČKA Aleš a 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, roč. 2005. Berlin: Springer Verlag, 2005, s. 371-375. ISBN 978-3-540-29105-3. ISSN 0302-9743. Detail
  • ČEŠKA Milan, KŘENA Bohuslav a 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: Universidad de Las Palmas de Gran Canaria, 2005, s. 161-164. ISBN 84-689-0432-5. Detail
  • ČEŠKA Milan, KŘENA Bohuslav a VOJNAR Tomáš. Parallel State Space Generation and Exploration on Shared-Memory Architectures. In: Computer Aided Systems Theory - EUROCAST 2005. Lecture Notes in Computer Science, roč. 3643. Berlin: Springer Verlag, 2005, s. 275-280. ISBN 978-3-540-29002-5. Detail
  • ČEŠKA Milan, ERLEBACH Pavel a 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, s. 101-117. Detail
  • JANOUŠEK Vladimír a KOČÍ Radek. PNtalk Project: Current Research Direction. In: Simulation Almanac 2005. Praha: Fakulta elektrotechniky ČVUT, 2005, s. 50-62. ISBN 80-01-03322-8. Detail
  • HABERMEHL Peter a VOJNAR Tomáš. Regular Model Checking Using Inference of Regular Languages. Electronic Notes in Theoretical Computer Science, roč. 138, č. 3, 2005, s. 21-36. ISSN 1571-0661. Detail
  • MAREK Vladimír. State-space Exploration of Petri Nets. In: Proceedings of 39th International Conference MOSIS '05. Ostrava: MARQ, 2005, s. 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: Fakulta informatiky MU, 2005, s. 145-154. Detail
  • SCHWARZ Ivan, ČEŠKA Milan a 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: MARQ, 2005, s. 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: Fakulta informačních technologií VUT v Brně, 2005, s. 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: Fakulta informačních technologií VUT v Brně, 2005, s. 668-672. ISBN 978-80-214-2890-4. Detail
  • JANOUŠEK Vladimír a KOČÍ Radek. Towards Model-Based Design with PNtalk. In: Proceedings of the International Workshop MOSMIC'2005. Žilina: Fakulta riadenia a informatiky Žilinskej Univerzity v Žiline, 2005, s. 59-66. ISBN 80-8070-468-6. Detail
  • ČEŠKA Milan a TURAKHODJAEVA Nasibakhon. Verification of Worklow Management Systems described by Object-Oriented Petri Nets. In: Proceedings of XXVIIth International Autumn Colloquium ASIS 2005. Ostrava: MARQ, 2005, s. 189-198. ISBN 80-86840-16-6. Detail
  • BOUAJJANI Ahmed, HABERMEHL Peter, MORO Pierre a 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, roč. 3440. Berlin: Springer Verlag, 2005, s. 13-29. ISBN 978-3-540-25333-4. Detail
  • KOČÍ Radek a TURAKHODJAEVA Nasibakhon. Workflow modeling with Petri nets in Workflow Management Systems. In: Proceedings of MOSIS'05. Ostrava: MARQ, 2005, s. 120-127. ISBN 80-86840-10-7. Detail

2004

  • BOUAJJANI Ahmed, HABERMEHL Peter a VOJNAR Tomáš. Abstract Regular Model Checking. Lecture Notes in Computer Science, roč. 2004, č. 3114, s. 372-386. ISSN 0302-9743. Detail
  • ČEŠKA Milan a 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, s. 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: MARQ, 2004, s. 73-80. ISBN 80-85988-98-4. Detail
  • HABERMEHL Peter a 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, s. 61-71. Detail
  • MAREK Vladimír. State-space Model Based on Graph Rewriting. In: Proceedings of 7th International Conference ISIM '04. Ostrava: MARQ, 2004, s. 133-140. ISBN 80-85988-99-2. Detail
  • JANOUŠEK Vladimír a 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, s. 31-36. ISBN 3-901608-28-1. Detail
  • ROGALEWICZ Adam a VOJNAR Tomáš. Tree Automata In Modelling And Verification Of Concurrent Programs. In: Proceedings of ASIS 2004. Ostrava: MARQ, 2004, s. 197-202. ISBN 80-86840-03-4. Detail
  • HRUBÝ Martin, JANOUŠEK Vladimír a KOČÍ Radek. Vývoj pokročilých metod modelování a protypování komplikovaných systémů. In: NETSS2004. Ostrava: MARQ, 2004, s. 103-108. ISBN 80-85988-92-5. Detail
Nahoru