A formal, graphical, executable technique for the specification and analysis of concurrent, discrete-event dynamic systems; a technique undergoing standardisation. More on Petri nets...
A specification in the form of a Petri net model may be formally analysed, to verify that static and dynamic system requirements are met. Methods available are based on Occurrence graphs (state spaces), Invariants and Timed Petri nets. The inclusion of timing enables performance analysis.
Modelling is an iterative process. At each iteration analysis may uncover errors in the model or shortcomings in the specification. In response the Petri net is modified and re-analysed. Eventually a mathematically correct and consistent model and specification is achieved.
Software tools exist which support and automate analysis.