A formal, graphical, executable technique for the specification and analysis of concurrent, discrete-event dynamic systems; a technique undergoing standardisation. More on Petri nets...
System requirements expressed and verified (by formal analysis) using the technique constitute a formal system specification.