A Time Abstraction Method for Efficient Verification of Communicating Systems

An important practical approach to automatic verification of finite state concurrent systems is temporal logic model checking. However, a major barrier towards wider application of suchmethods is the state explosion problem that often occurs during the composition of complex communicating systems. In addition to being large, many systems have very deep state spaces as well. In this paper, we propose an abstraction method based on time abstraction which can significantly reduce both the size as well as the depth of the state space that must be explored during model checking. It is especially suited for applications involving systems that are loosely coupled in the sense that communication activity is relatively sparse, such as applications involving DSPs, which have large intervals of autonomous processing, with communication activity in between. All properties expressiblewith the temporal logic CTL* or CTL* -X are strongly preserved under the proposed abstraction. In particular, we give a method that can replace a chain of states by a single state with atime label . The abstractedmodel is represented by means of atimed label transition system model. We give acomposition algorithm for composing the individually time abstracted models to form a global model that can be converted back to a conventional, but potentiallymuch reduced,state space suitable formodel checking. Furthermore, a similar approach can be followed in dealing with wait states in which a system is idling while waiting for an escape signal. For many cases, our approach is successful in alleviating the state explosion problemthat often arises in composition of communicating systems.