| Popis: |
The advent of ever more complex reactive systems in increasingly critical areas calls for the development of automated verification techniques. Model checking is one such technique, which has proven quite successful. However, the state explosion problem remains the stumbling block in many situations. Recent experience indicates that solutions are to be found in the application of techniques for property preserving abstraction and successive approximation of models. Most such applications have so far been based on the property-preserving characteristics of simulation relations. A major drawback of all these results is that they do not offer a satisfactory formalization of the notions of precision and optimality of abstractions. Furthermore, the use of simulation relations poses difficulties when formalizing the preservation of both existential and universal properties over the same abstract domain. The theory of Abstract Interpretation offers a framework for the definition and justification of property preserving abstractions. Furthermore, it provides a method for the effective computation of abstract models directly from the text of a program, thereby avoiding the need for intermediate storage of a full-blown model. Finally, it formalizes the notion of optimality, while allowing to trade precision for speed by computing sub-optimal approximations. However, Abstract Interpretation has traditionally been focussed on the analysis of deterministic programs, in particular through abstractions that preserve invariance properties, i.e., properties that hold in all states along every possible execution path. In this paper, we extend Abstract Interpretation to non-deterministic systems. This results in a uniform basis for the analysis of both existential and universal reactive properties, as expressible in the branching time logic CTL*. It is shown how optimal abstract models may be constructed by symbolic execution of programs and that approximation may be used to find an optimum between precision and speed. Examples are given to illustrate this. We indicate conditions under which also the falsity of formulae is preserved. Finally, we compare our approach to those based on simulation relations. |
