Veranstaltung

Tools:
Tina [https://projects.laas.fr/tina/index.php](https://projects.laas.fr/tina/index.php)
CPN Tools [https://cpntools.org/](https://cpntools.org/)

References:
Zaitsev D.A. Clans of Petri Nets: Verification of protocols and performance evaluation of networks, LAP LAMBERT Academic Publishing, 2013, 292 p. ([http://daze.ho.ua/daze-clans-covered-draft.djvu](http://daze.ho.ua/daze-clans-covered-draft.djvu))
Zaitsev D.A., Shmeleva T.R. Simulating Telecommunication Systems with CPN Tools: Students' book // Odessa: ONAT, 2006. - 60 p. ([http://daze.ho.ua/cpnmp2.pdf](http://daze.ho.ua/cpnmp2.pdf))
Recent developments in papers on [http://daze.ho.ua](http://daze.ho.ua/)

A system should be correct and efficient. We specify discrete event systems by Petri nets to apply formal analysis techniques based on graph theory and linear algebra to prove correctness. Extended models, such as colored Petri nets, are applied to implement performance evaluation via simulation. We start from case studies using the modeling system Tina and its facilities of model checking for verification of communication protocols. Then we apply Petri nets for the control of robotic manufacturing and consider the sharing of resources in automated manufacturing. Colored Petri nets allow more precise specification of systems, which also leads to reduced abilities for applying formal techniques. So the basic method of investigation is simulation. Our case study concerns modern technology of networking and models are supplied with measuring components which compute statistical characteristics directly in the process of simulation. Finally, a review of modern theory of infinite Petri nets and Sleptsov net computing are provided with a view on cybersecurity of intelligent grids and clouds and hyper-performance concurrent computations.