The increasing complexity of the business processes requires automated methods for trouble-shooting and debugging of the process model in operation. This paper proposes mechanism of fault detection based on the concept of backwards reachability for the coloured workflow nets. The formal verification methods defined for coloured Petri nets such as state space method or place invariants declaration suffer from fast-growing computational complexity. The article offers the set of firing rules for backwards token-play on coloured workflow net. This method helps to detect resource-related failures of the two most common types: ”the missing arc” fault (the resource was not initialized) and ”wrong expression fault” (there is no proper resource).

The design of complex distributed automation systems often presents great challenges due to the size and number of components which have to work in parallel to one another in real time. This paper discusses some of the problems of designing such systems. The use of colored dynamic state diagrams for the modeling of complex real-time systems is suggested as a possible solution. This type of diagram is based on State Charts, the well-known and generally applied description technique included as one variation in the unified modeling language. Colored State Charts harness two techniques: the modelling technique well accepted by engineers, and high level Petri nets with their outstanding powers of description. By coloring State Charts, the behaviour of several objects or processes can be modelled simultaneously in a single figure. The colored state diagrams contain a variety of resources to facilitate clear and unequivocal representation of the composition of a number of simple state diagrams. They also have additional mechanisms for mapping the dependencies and relationships between individual objects. Via transformation into colored Petri nets, they make formal verification possible. Their usability is shown in a modelled reference example.