A formal, graphical,
executable technique for the
specification and analysis of
concurrent, discrete-event dynamic
systems; a technique undergoing standardisation.
More on Petri nets...
The technique is mathematically defined. Many
static and dynamic properties of a Petri net (and hence a system specified
using the technique) may be mathematically proven. More on Formal Methods...