Project detail

Automated methods and tools supporting development of reliable parallel and distributed systems

Duration: 01.01.2004 — 31.12.2006

Funding resources

Czech Science Foundation - Standardní projekty

- whole funder (2004-01-01 - 2006-12-31)

On the project

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.

Description in English
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.

Keywords
Modeling, simulation, verification, prototyping, parallel, distrubuted

Key words in English
Modeling, simulation, verification, prototyping, parallel, distrubuted

Mark

GA102/04/0780

Default language

Czech

People responsible

Haša Luděk, Ing. - fellow researcher
Janoušek Vladimír, doc. Ing., Ph.D. - fellow researcher
Kočí Radek, Ing., Ph.D. - fellow researcher
Křena Bohuslav, Ing., Ph.D. - fellow researcher
Rábová Zdeňka, doc. Ing., CSc. - fellow researcher
Vojnar Tomáš, prof. Ing., Ph.D. - fellow researcher
Češka Milan, prof. RNDr., CSc. - principal person responsible

Units

Faculty of Information Technology
- beneficiary (2004-05-13 - not assigned)

Results

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

JANOUŠEK, V., KIRONSKÝ, E. SmallDEVS-2006-07-18 (1. verze s GUI). Bern: Squeak Foundation, 2006.
Detail

HAŠA, L., ČEŠKA, M. 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. p. 269-274. ISBN: 980-6560-19-1.
Detail

JANOUŠEK, V., KOČÍ, R. 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. p. 31-36. ISBN: 3-901608-28-1.
Detail

ROGALEWICZ, A., VOJNAR, T. Tree Automata In Modelling And Verification Of Concurrent Programs. In Proceedings of ASIS 2004. Ostrava: 2004. p. 197-202. ISBN: 80-86840-03-4.
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

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

ERLEBACH, P. Experience from Verifying in TVLA. In EEICT'05. volume 3. Brno: Faculty of Electrical Engineering and Communication BUT, 2005. p. 648-652. ISBN: 80-214-2890-2.
Detail

JANOUŠEK, V., KOČÍ, R. 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. p. 59-66. ISBN: 80-8070-468-6.
Detail

VOJNAR, T., ČEŠKA, M., ERLEBACH, P. 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. p. 101-117.
Detail

ČEŠKA, M., TURAKHODJAEVA, N. Verification of Worklow Management Systems described by Object-Oriented Petri Nets. In Proceedings of XXVIIth International Autumn Colloquium ASIS 2005. Ostrava: 2005. p. 189-198. ISBN: 80-86840-16-6.
Detail

MAREK, V. State-space Exploration of Petri Nets. In Proceedings of 39th International Conference MOSIS '05. Ostrava: 2005. p. 114-119. ISBN: 80-86840-10-7.
Detail

MAREK, V. State-space Model Based on Graph Rewriting. In Proceedings of 7th International Conference ISIM '04. Ostrava: 2004. p. 133-140. ISBN: 80-85988-99-2.
Detail

ERLEBACH, P. 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. p. 145-154.
Detail

ČEŠKA, M., KŘENA, B., VOJNAR, T. 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. p. 161-164. ISBN: 84-689-0432-5.
Detail

ERLEBACH, P., VOJNAR, T. 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. p. 219-226. ISBN: 80-86840-09-3.
Detail

JANOUŠEK, V., SLAVÍČEK, P. Concept for the parallel road-traffic simulation. In Proceedings of MOSIS'05. Ostrava: 2005. p. 123-128. ISBN: 80-86840-10-7.
Detail

SCHWARZ, I., ČEŠKA, M., JANOUŠEK, V. Towards an Implementation of Distributed PNtalk. In Proceedings of 39th Spring International Conference MOSIS'05 Modelling and Simulation of Systems. Ostrava: 2005. p. 166-173. ISBN: 80-86840-10-7.
Detail

ROGALEWICZ, A. 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. p. 663-667. ISBN: 80-214-2890-2.
Detail

KOČÍ, R., TURAKHODJAEVA, N. Workflow modeling with Petri nets in Workflow Management Systems. In Proceedings of MOSIS'05. Ostrava: 2005. p. 120-127. ISBN: 80-86840-10-7.
Detail

BOUAJJANI, A., HABERMEHL, P., ROGALEWICZ, A., VOJNAR, T. Abstract Regular Tree Model Checking. In 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

JANOUŠEK, V.; POLÁŠEK, P.; SLAVÍČEK, P. Metajazyk pro popis DEVS formalismu. In 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. In ISC 2006 Proceedings. Zwijnaarde: 2006. p. 69-73. ISBN: 90-77381-26-0.
Detail

ČEŠKA, M.; JANOUŠEK, V.; KOČÍ, R.; KŘENA, B.; VOJNAR, T. PNtalk: State of the Art. In Proceedings of the Fourth International Workshop on Modelling of Objects, Components, and Agents. Hamburg: 2006. p. 301-307.
Detail

KOČÍ, R.; TURAKHODJAEVA, N. Modeling Workflow Using Object Oriented Petri Nets. In Proceedings of ASIS'06. Ostrava: 2006. p. 127-132. ISBN: 8086840263.
Detail

JANOUŠEK, V.; KOČÍ, R. 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

KŘENA, B. Computer Go as a Verification Case Study. In Proceedings of XXVIIIth International Autumn Colloquium ASIS 2006: Advanced Simulation of Systems. Ostrava: 2006. p. 95-100. ISBN: 80-86840-26-3.
Detail

JANOUŠEK, V. On the Prototype-Based Object Orientation in Modeling and Simulation. In Proceedings of of Advanced Simulation of Systems 2006. Ostrava: 2006. p. 1-0. 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

JANOUŠEK, V.; KIRONSKÝ, E. SmallDEVS, an Interactive Modeling and Simulation Tool for Smalltalk. In Proc. of MOSIS'06. Ostrava: 2006. p. 91-98. ISBN: 80-86840-21-2.
Detail

JANOUŠEK, V.; KIRONSKÝ, E. Exploratory Modeling with SmallDEVS. In Proc. of ESM 2006. Ghent: EUROSIS, 2006. p. 122-126. ISBN: 90-77381-30-9.
Detail

ERLEBACH, P.; ČEŠKA, M.; VOJNAR, T. 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. p. 181-182. ISBN: 978-3-540-75866-2.
Detail

KŘENA, B., ČEŠKA, M., VOJNAR, T. Parallel State Space Generation and Exploration on Shared-Memory Architectures. In Computer Aided Systems Theory - EUROCAST 2005. Lecture Notes in Computer Science 3643. Berlin: Springer Verlag, 2005. p. 275-280. ISBN: 978-3-540-29002-5.
Detail

MATOUŠEK, P., SMRČKA, A., VOJNAR, T. High-Level Modelling, Analysis, and Verification on FPGA-Based Hardware Design. In 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

BOUAJJANI, A.; HABERMEHL, P.; ROGALEWICZ, A.; VOJNAR, T. Abstract Regular Tree Model Checking of Complex Dynamic Data Structures. In Static Analysis. LNCS 4134. Berlin: Springer Verlag, 2006. p. 52-70. ISBN: 978-3-540-37756-6.
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

HABERMEHL, P.; IOSIF, R.; VOJNAR, T. Automata-based Verification of Programs with Tree Updates. In Tools and Algorithms for the Construction and Analysis of Systems. LNCS 3920. Berlin: Springer Verlag, 2006. p. 350-364. ISBN: 978-3-540-33056-1.
Detail

VOJNAR, T., BOUAJJANI, A., HABERMEHL, P., MORO, P. Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. In Tools and Algorithms for the Construction and Analysis of Systems. LNCS 3440. Berlin: Springer Verlag, 2005. p. 13-29. ISBN: 978-3-540-25333-4.
Detail

IOSIF, R.; HABERMEHL, P.; VOJNAR, T.; BOUAJJANI, A.; BOZGA, M.; MORO, P. Programs with Lists are Counter Automata. In Computer Aided Verification. LNCS 4144. Berlin: Springer Verlag, 2006. p. 517-531. ISBN: 978-3-540-37406-0.
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

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

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

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

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

JANOUŠEK, V., KOČÍ, R. PNtalk Project: Current Research Direction. In Simulation Almanac 2005. Praha: Faculty of Electrical Engineering, 2005. p. 50-62. ISBN: 8001033228.
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

ROGALEWICZ, A. Verification of Programs with Complex Data Structures. Brno: 2007. 122 p. ISBN: 978-80-214-3548-3.
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

JANOUŠEK, V. SmallDEVS-2004-03-19. Bern: Squeak Foundation, 2004.
Detail

JANOUŠEK, V. SmallDEVS-2005-02-21. Bern: Squeak Foundation, 2005.
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

Responsibility: Češka Milan, prof. RNDr., CSc.