A time abstraction method for efficient verification of communicating systems
Eric Verlind, Tilman Kolks, Gjalt de Jong, Bill Lin, Hugo De Man · 1994
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 such methods 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 expressible with 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 a time label.The abstracted model is represented by means of a timed label transition system model.We give a composition algorithm for composing the individually time abstracted models to form a global model that can be converted back to a conventional, but potentially much reduced,state space suitable for model 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 problem that often arises in composition of communicating systems.