Projekt vychází z původního matematického modelu objektově orientovaných Petriho sítí (OOPN), který byl vytvořen na ÚIVT FEI VUT a který spojuje výhody vysokoúrovňových Petriho sítí s výhodami objektově orientovaných návrhových technologií. Projekt sleduje dva hlavní cíle. Prvním cílem je návrh a implementace systému pro modelování, simulaci a prototypování distribuovaných aplikací s využitím OOPN, včetně možnosti distribuovaného běhu vytvořených prototypů a propojení s objekty implementovanými jiným způsobem. Druhým cílem je umožnit formální analýzu a verifikaci modelů popsaných OOPN, a to zejména s využitím jejich vhodně redukovaných stavových prostorů. To si vyžádá originální řešení některých specifických teoretických problémů plynoucích z dynamické instanciace objektů. Dále bude posouzena možnost aplikace metod modulární či kompozitní analýzy a také metod statické analýzy OOPN. Navržené nástroje pro modelování, prototypování a verifikaci budou zastřešeny metodologií doporučující způsob jejich použití při návrhu distribuovaných aplikací tak, aby se dosáhlo dobré udržovatelnosti, spolehlivosti a výkonnosti.

Description in English
The project builds upon the original mathematical concept of object-oriented Petri nets (OOPNs) which has been proposed at the Department of Computer Science and Engineering of the Technical University in Brno and which combines advantages of high-level Petri nets and object-oriented design technologies. The project comes with two main goals. The first goal is to design and implement a tool for modelling, simulation, and prototyping distributed applications using OOPNs, including the possibility of running prototypes of applications in a truly distributed way and interconnecting them with external objects. The second goal is to allow for formal analysis and verification of OOPN-based models using especially their suitably reduced state spaces. This requires an original solution of some specific theoretical problems stemming from the dynamic instantiation of objects. Moreover, the possibility of modular and compositional analysis, as well as static analysis will be evaluated. The proposed conceptual and computer-aided tools for modelling, prototyping, and verification will be integrated by a methodology suggesting how they should be used for designing complex distributed applications in order to achieve their high maintainability, reliability, and effectiveness.

GA102/00/1017

Czech

Češka Milan, prof. RNDr., CSc. - principal person responsible
Haša Luděk, Ing. - fellow researcher
Kočí Radek, Ing., Ph.D. - fellow researcher
Křena Bohuslav, Ing., Ph.D. - fellow researcher
Schwarz Ivan, Ing. - fellow researcher

Department of Intelligent Systems
- responsible department (23.10.2001 - not assigned)
Faculty of Information Technology
- responsible department (1.1.2001 - not assigned)
Automated Analysis and Verification Research Group - VeriFIT
- internal (23.10.2001 - 31.12.2002)
Petri Nets Research Group
- internal (23.10.2001 - 31.12.2002)
System Modelling and Optimization Research Group
- internal (23.10.2001 - 31.12.2002)
Faculty of Information Technology
- co-beneficiary (23.10.2001 - 31.12.2002)
Faculty of Information Technology
- beneficiary (1.1.2001 - not assigned)

HOLUB, O.; KUNOVSKÝ, J.; MELKES, F. The examples of the TKSL/C. Proccedings of 4th International Scientific Conference ELECTRONIC COMPUTERS & INFORMATICS. Košice: unknown, 2000. p. 98-101. ISBN: 80-88922-25-9.
Detail

KUNOVSKÝ, J.; POSPÍŠIL, P.; SEZEMSKÝ, P. Implicit solution of kinetics in HV circuit breakers. Proceedings of 3rd Mathmod. Vienna: unknown, 2000. p. 11-11. ISBN: 3-901608-15-X.
Detail

KUNOVSKÝ, J. Real-Time Applications of the Taylor Series. Proceedings of ADIUS 2000, ADI. Boston: unknown, 2000. p. 67-75.
Detail

MAREK, V. Category of Markov Systems. Proceedings of the 34th International Conference: Modelling and Simulation of Systems - MOSIS 2000. Rožnov pod Radhoštěm: Marq software s.r.o., 2000. p. 75-80. ISBN: 80-85988-44-5.
Detail

ČEŠKA, M.; JANOUŠEK, V.; VOJNAR, T. Generating and Exploiting State Spaces of Object-Oriented Petri Nets. Proceedings of Workshop on Software Engineering and Petri Nets, 21st International Conference on Application and Theory of Petri Nets 2000. Aarhus: unknown, 2000. p. 35-54. ISSN: 0105-8517.
Detail

ČEŠKA, M.; JANOUŠEK, V.; VOJNAR, T. PNtalk Modelling Experience. Proceedings of 26th ASU Conference, Object Oriented Modelling and Simulation 2000. La Valetta: unknown, 2000. p. 65-73.
Detail

VOJNAR, T. Towards Formal Analysis and Verification over State Spaces of Object-Oriented Petri Nets. Brno: 2001. p. 0-0.
Detail

ČEŠKA, M.; JANOUŠEK, V.; VOJNAR, T. Modelling, prototyping, and verifying concurrent and distributed applications using object-oriented Petri nets. Kybernetes: The International Journal of Systems Cybernetics, 2002, vol. 2002, no. 9, p. 1289-1299. ISSN: 0368-492X.
Detail

ČEŠKA, M.; JANOUŠEK, V.; VOJNAR, T. Analysis and Verification Queries over Object-Oriented Petri Nets. Lecture Notes in Computer Science, 2001, vol. 2001, no. 2178, p. 365-384. ISSN: 0302-9743.
Detail

ČEŠKA, M.; JANOUŠEK, V.; VOJNAR, T. Generating and Using State Spaces of Object-Oriented Petri Nets. International Journal of Computer Systems Science and Engineering, 2001, vol. 16, no. 3, p. 183-193. ISSN: 0267-6192.
Detail

JANOUŠEK, V.; SLAVÍČEK, P. Heterogenní simulace na bázi DEVS. Proceedings of XXVth International Autumn Colloquium ASIS 2003. Ostrava: Marq software s.r.o., 2003. s. 213-218. ISBN: 80-58988-88-7.
Detail

SCHWARZ, I. Architecture of Distributed Simulator of PNtalk. Proceedings of 36th International Conference MOSIS'02 Modelling and Simulation of Systems. Vol. I. Ostrava: Marq software s.r.o., 2002. p. 81-88. ISBN: 80-85988-71-2.
Detail

KŘENA, B.; VOJNAR, T.; ČEŠKA, M. Integrated Type Analyzer and State Space Generator of Object-Oriented Petri Nets. Brazilian Petri Net Meeting. Natal: 2002. p. 0-0.
Detail

JANOUŠEK, V.; KOČÍ, R. PNtalk - An Open System for Prototyping and Simulation. Proceedings of The 28th ASU Conference. ASU Newsletter. Brno: Faculty of Information Technology BUT, 2002. p. 133-146. ISSN: 1102-593X.
Detail

KOČÍ, R.; RÁBOVÁ, Z. The PNtalk System and Interoperability. Proceedings of International Conference MOSIS '02. Vol. 1. Ostrava: Marq software s.r.o., 2002. p. 73-80. ISBN: 80-85988-71-2.
Detail

ČEŠKA, M.; HRUŠKA, T.; ZENDULKA, J. Education in Information Technology at Brno University of Technology. Proceedings of the International Conference - Advances in Infrastructure for e-business, e-education, e-science, and e-medicine on the Internet. L'Aquila: SSGRR Telecom Italia Learning Services, 2002. p. 1-7. ISBN: 88-85280-62-5.
Detail

KŘENA, B. First Approach to Model Checking in Object-Oriented Petri Nets. Proceedings of XIIIrd International Autumn Colloquium ASIS 2001 Advanced Simulation of Systems. Ostrava: Marq software s.r.o., 2001. p. 105-110. ISBN: 80-85988-61-5.
Detail

KOČÍ, R. The PNtalk System - a Technique for Object Oriented Modelling. Proceedings of XXIIIrd International Autumn Colloquium. Ostrava: Marq software s.r.o., 2001. p. 151-158. ISBN: 80-85988-61-5.
Detail

JANOUŠEK, V.; SCHWARZ, I. Interoperability of Object Oriented Petri Nets. Proc. of MOSIS'01. Ostrava, Czech Republic: Marq software s.r.o., 2001. p. 137-144. ISBN: 80-85988-57-7.
Detail

KOČÍ, R.; VOJNAR, T. A PNtalk-based Model of a Cooperative Editor. Proceedings of the 35th Spring International Conference on Modelling and Simulation of Systems -- MOSIS 2001. Hradec nad Moravicí, Czech Republic: Marq software s.r.o., 2001. p. 165-172. ISBN: 80-85988-57-7.
Detail

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