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...