Hierarchical reduction and refinement checking for asynchronous processes

Given a system model and a predicate over current and new variables, the transition invariant checking problem is to check whether all transitions of the system satisfy the given predicate. It is one of the fundamental problems in computer aided verification. The worst-case complexity of the problem grows exponentially in terms of the model description. In this work, a theory for asynchronous processes is developed in the hope of alleviating the infamous state explosion problem. The basic idea is to merge multiple unobservable transitions in a hierarchical way and thus reduce unnecessary interleavings of steps in different processes. Both explicit and implicit algorithms are designed to realize the new theory. The experimental results show that the new algorithms perform better in both cases. For verification, we focus on the problem of refinement checking, that is, establishing that the set of behaviors allowed by implementation is included in specification. In this paradigm, an implementation model is checked against its specification. If all specification variables appear in the implementation, the problem can be solved by transition invariant checking. A heuristic is proposed to assign values to specification variables in case they are missing in the implementation. The proposed heuristic can be implemented by automatic syntactic translation. It also works in sync with the new transition checking algorithms. Along with the compositional reasoning rules, these three techniques constitute a set of tools for checking asynchronous systems. Finally, some network protocols and their implementations are checked as illustrations. The detailed discussion will shed light on practical verification and implementation issues