On the fly Distributed Verification
Blaise Genest
IRISA, Rennes, France.
07-11-07

---

Abstract

There are many cases where we cannot apply model-checking. For instance, we do not always have a model of the system, since it may be partially unknown, too big, or simply the system evolve in an unknown way. It is in particular the case for distributed systems, where processes can appear and disappear. Instead of model-checking statically before starting of the system, we want to supervise dynamically processes to know whether some property holds or not. For instance, we want to detect whether some accident occurred, and then ask the supervisor to trigger an alarm.

We study the feasibility of distributed dynamic verification, and the complexity of the supervisor in case they are doable. The main technique used is to make an analogy between on the fly distributed verification and implementation. Then, we can use the numerous results for implementation in order to solve on the fly distributed verification, in particular Zielonka's algorithm.

Work in progress, joint with Doron Peled.