Extended Coloured Petri Nets with structured Tokens Formal Method for Distributed Systems

Demands for clarity, reliability, productivity and the increasing complexity of communication software, protocols and algorithms require development of methods to ensure consistent, unambiguous, formal and accurate representation. In this article, a formal method is developed based on coloured Petri nets (CPN). This method represents an extended class of Petri nets; it is named High Coloured Petri Nets with Structured Tokens (HCPN-ST). CPN are extended with structured tokens, which contain an ordered sequence of colours and carry additional information like events, operations, network nodes, etc. Furthermore the firing condition includes logical expressions. A formal definition of these nets is introduced, including its token structures and firing rules, which allow checking single token elements, parts of the token sequences or Boolean conditions between them. As an example, an algorithm that operates on P2P networks is modeled with the developed method. This example demonstrates analysis of such nets. It is transformed into CPN, in order to simulate, analyze and verify it with software tools. Then CPN model is simulated and analyzed with a tool named PENECA Chromos. In order to verify some properties this tool interoperates with the well known INA tool. So this formal method is demonstrated as an effective method to model and analyze distributed systems.