Error diagnosis in finite communicating systems

Abstract

We present an error diagnosis method for parallel communicating systems with branching temporal specifications. Verification is done by model checking on the finite graph of the executions. We consider errors whose diagnostics are sequences of the graph. We define a minimality criterium for the diagnostics such that a finite number of minimal diagnostics give all the reasons of the error. Diagnostics are produced in a simplified form according to a given abstraction. We define an equivalence on models which preserves the simplified diagnostics.