A formal Modeling method based on CPN

As a method of system modeling, Coloured Petri nets occupy an essential position in the fields of discrete events and dynamic systems. Traditional Coloured Petri Net is defined with multi-sets that made it difficult in the modeling formalization and difficult to understand in computing. In this paper, a new method to describe Coloured Petri Net with formalization mathematics is presented. In this research, multi-sets can be see as the product of two matrixes and CPN is a superposed net of series of Petri Nets with the same base net. In order to describe CPN with mathematics method effectively, a new concept named as 'Coloured Token Vector' is presented. As a case, routing protocols self-switch mechanism architecture for sensor networks is outlined, the mechanism modeled on the basis of CPN; this is the first such analysis of routing protocols self-switch mechanism in sensor networks, which is simple for use and effective modeling formalization.