Stochastic Well-Formed coloured nets and multiprocessor modelling applications

The new class of Stochastic Well-formed coloured Nets (SWN) is defined as a syntactic restriction of Stochastic High-Level Nets. The interest of the introduction of restrictions in the model definition is the possibility of exploiting the Symbolic Reachability Graph (SRG) to reduce the complexity of Markovian performance evaluation with respect to classical Petri net techniques. It turns out that SWNs allow the representation of any colour function in a structured form, so that any unconstraint high-level net can be transformed into a well formed net. Moreover, most constructs useful for the modelling of distributed computer systems and architectures directly match the “well form” restriction, without any need of transformation. A non trivial example of the usefulness of the technique in the performance modelling and evaluation of multiprocessor architectures is included.