Petri Nets: A Formal Language to Specify and Verify Concurrent Non-Deterministic Event Systems

Abstract

The study of concurrent and parallel systems has been a challenging research domain within cyberphysical systems community. This chapter provides a pragmatic introduction to the creation and analysis of such system models using the popular Petri nets formalism. Petri nets is a formalism that convinces through its simplicity and applicability.We offer an overview of the most important Petri nets concepts, analysis techniques and model checking approaches. Finally, we show the use of so-called High-level Petri nets for the representation of complex data structures and functionality and present a novel research approach that allows the use of Petri nets inside Functional Mock-up Units and cyber-physical system models.