Inconsistent State Analysis of a Network Receiver with Colored Petri Nets

This paper deals with a new method to study dependability of distributed systems using Colored Petri Nets (CPN) which are a powerful, recognized and intuitive modelling tool. They allow a precise representation of the studied systems. The CPN analysis gives information about static and dynamic behavior of the modelled system and can be used to study questions concerning its dependability. This paper develops a new method of CPN analysis called the Backward reachability. It provides information about different ways of reaching a particular CPN marking that represent, for example, a failure state or a transilient fault. This analysis is performed on an inverse CPN which is obtained by transforming original CPN structure. The illustrative case is the study of a communication protocol composed of three parts: the sender, the receiver and the network. The Backward reachability analysis done on this system starts by supposing an inconsistent sate in the receiver and looks for the corresponding sender state. The main advantage of this method is that it determines the sequence leading from the initial to the final state independently on the final marking value.