Stochastic Petri net-based modeling and formal analysis of fault tolerant Contract Net Protocol

Contract Net Protocol (CNP) is probably the most widely used task allocation protocol in distributed multi-agent systems (MAS). To cope with real-world applications, this protocol must be expanded by addressing some major challenging issues in the current distributed systems. Temporal interaction aspects and reliability issues of such systems, critical to guaranteeing performance, are the focus of this paper. Many researchers have proposed various methods to expand and to improve CNP but those challenges have not been much addressed in a formal way. To cope with these limitations, this paper proposes a Petri net-based model that extends the conventional contract net with real time constraints, often defined as interaction duration and message deadlines, and fault tolerance to handle the agent death exception. Our aim is, hence, to devise an extended CNP that achieves the reliability of the manager agent in the case of contractor crash failure while operating in an open and large scale multi-agent system under time constraints. To address the challenge problem of crash failure detection of the contractor in CNP, we propose to formally model the watchdog/heartbeat mechanism into the communication between the manager and the contractor. Using such mechanism, the manager can detect the crash failure on time and may hence trigger an appropriate recovery procedure to move the system into a safe and a consistent state. The proposed extended CNP model is developed using stochastic timed colored Petri nets which include systematic specification, design and implementation of components of the system. Various useful results will be drawn by simulation as well as state space analysis. This formal analysis shows that the protocol terminates correctly either in a safety case or in a failure situation. It also proves that the protocol meets the key properties namely model correctness, deadline respect, absence of deadlocks and livelocks, absence of dead code, agent terminal states consistency, concurrency, and validity.