Formal Verification of Mutual Exclusion Between the Guards of Deterministic Choice Structures

The formal verification of mutual exclusion between the guards of a deterministic choice structure is of great interest to the asynchronous circuit designers. To perform this spot of checking, we propose a treatment in two phases; the first is based on a static analysis, the mutual exclusion (ME) is checked using a symbolic decision tool. In the second phase, if the static analysis returns a result like "the model does not satisfy mutual exclusion", the dynamic verification takes into account the constraints of the environment to refine the analysis. If the mutual exclusion is still not satisfied, it gives a counter-example. The principle is to check whether indeterminism exists during the construction of the whole execution model, using a model-checking tool.