Reachability Analysis via Specialization of Constraint Logic Programs

Fabio Fioravanti¹, Alberto Pettorossi², Maurizio Proietti³, Valerio Senni²

¹Dipartimento di Scienze, University `G. D’Annunzio’, Pescara, Italy
²DISP, University of Rome Tor Vergata, Rome, Italy
³CNR-IASI, Rome, Italy

1 Reachability Analysis of Infinite State Systems

One of the present challenges in the field of automatic verification of reactive systems is the extension of the model checking techniques [4] to systems with an infinite number of states. For these systems exhaustive state exploration is obviously impossible and, even for restricted classes, simple properties such as safety (or reachability) properties are undecidable.

In order to overcome this limitation, several verification tools make use of constraints over the integers Ζ (or the reals R) to represent infinite sets of states (see, for instance, [1,3,6,11,13,19]). By manipulating constraint-based representations of sets of states, one can verify a safety property φ of an infinite state system by one of the following two strategies:

(i) Backward Strategy: one applies a backward reachability algorithm, thereby computing the set BR of states from which it is possible to reach an unsafe state (that is, a state where ¬φ holds), and then one checks whether or not BR has an empty intersection with the set I of the initial states;

(ii) Forward Strategy: one applies a forward reachability algorithm, thereby computing the set FR of states reachable from an initial state, and then one checks whether or not FR has an empty intersection with the set U of the unsafe states.

Variants of these two strategies have been proposed and implemented in the above mentioned automatic verification tools. Some of them also use techniques borrowed from the field of abstract interpretation [5], whereby in order to check whether or not a safety property φ holds for all states which are reachable from the initial states, an upper approximation BR (or FR) of the set BR (or FR) is computed. These techniques improve the termination of the verification tools at the expense of a possible loss of precision. Indeed, whenever BR ∩I ≠ ∅ (or FR ∩U ≠ ∅), one cannot conclude that, for some state, φ does not hold.

One weakness of the Backward Strategy is that, when computing BR, it does not take into account the properties holding in the initial states. This may lead, even if the formula φ does hold, to a failure of the verification process, because either the computation of BR does not terminate or one gets an overly approximated BR with a non-empty intersection with the set I. A similar weakness is also present in the Forward Strategy as it does not take into account the properties holding on the unsafe states when computing FR or  FR.

2 Improving Reachability Analysis by Program Specialization

We have developed a method, based on program specialization [12,14], for overcoming the weaknesses of Backward and Forward Strategies. Program specialization is a program transformation technique that, given a program and a specific context of use, derives a specialized program that is more effective in the given context. Our specialization method is applied before computing BR (or FR). Its objective is to transform the constraint-based specification of a reactive system into a new specification that, when used for computing BR (or FR), takes into consideration also the properties holding on the initial states (or the unsafe states, respectively).

Our method consists of the following three steps:
(1) the translation of a reactive system specification into a constraint logic program (CLP) that implements backward (or forward) reachability;
(2) the specialization of the CLP program with respect to the initial states (or the unsafe states, respectively), and
(3) the reverse translation of the specialized CLP program into a specialized reactive system.

The core of our specialization method is an algorithm that makes use of the definition introduction, unfolding, clause removal, and folding rules for transforming constraint logic programs (see, for instance, [7]).

An important feature of our specialization algorithm is that the applicability conditions of the transformation rules used by the algorithm are expressed in terms of the unsatisfiability (or entailment) of constraints on the domain R of the real numbers, instead of the domain Ζ of the integer numbers, thereby allowing us to use more efficient constraint solvers (according to the present state-of-the-art solvers). Note that, despite this domain change from Ζ to R, program specialization preserves the least model semantics of CLP(Ζ) programs. This result is based on the correctness of the transformation rules [7] and on the fact that the unsatisfiability (or entailment) of constraints on R implies the unsatisfiability (or entailment) of those constraints on Ζ. As a consequence of the correctness of (1) the translation, (2) the specialization, and (3) the reverse translation, our method is guaranteed to transform a given reactive system specification into one which satisfies the same safety properties.

The termination of the specialization algorithm is ensured by the fact that we use suitable generalization operators, similar to the widening operator introduced in the field of abstract interpretation [5].

A more detailed presentation of our specialization method appears in [10].

3 Experimental Evaluation

We have implemented our specialization method on the MAP transformation system for CLP programs [16], a tool for transforming CLP programs which uses the SICStus Prolog clpr library to operate on constraints on the reals. Then, we have performed experiments on several infinite state systems by using the Action Language Verifier (ALV), which is tool based on a BDD-based symbolic manipulation for enumerated types and on a solver for linear constraints on integers [19]. ALV performs backward and forward reachability analysis by an approximate computation of the least fixpoint of the transition relation of the system. We have run ALV using the options: `default’ and `A’ (both for backward analysis), and the option `F’ (for forward analysis). All experiments were performed on an Intel Core 2 Duo E7300 2.66 GHz under Linux.

The results of our experiments are reported in Table 1, where we have indicated, for each system and for each ALV option used, the following times expressed in seconds:

(i) the time taken by ALV for verifying the given system (columns Sys), and

(ii) the total time taken by MAP for specializing the system and by ALV for verifying the specialized system (columns SpSys).

	default		A		F
EXAMPLES	Sys	SpSys	Sys	SpSys	Sys	SpSys
1. Bakery2	0.03	0.05	0.03	0.05	0.06	0.04
2. Bakery3	0.70	0.25	0.69	0.25	∞	3.68
3. MutAst	1.46	0.37	1.00	0.37	0.22	0.59
4. Peterson	56.49	0.10	∞	0.10	∞	13.48
5. Ticket	∞	0.03	0.10	0.03	0.02	0.19
6. Berkeley RISC	0.01	0.04	⊥	0.04	0.01	0.02
7. DEC Firefly	0.01	0.02	⊥	0.03	0.01	0.07
8. IEEE Futurebus	0.26	0.68	⊥	⊥	∞	∞
9. Illinois University	0.01	0.03	⊥	0.03	∞	0.07
10. MESI	0.01	0.02	⊥	0.03	0.02	0.07
11. MOESI	0.01	0.06	⊥	0.05	0.02	0.08
12. Synapse N+1	0.01	0.02	⊥	0.02	0.01	0.01
13. Xerox PARC Dragon	0.01	0.05	⊥	0.06	0.02	0.10
14. Barber	0.62	0.21	⊥	0.21	∞	0.08
15. Bounded Buffer	0.01	3.10	0.01	3.16	∞	0.03
16. Unbounded Buffer	0.01	0.06	0.01	0.06	0.04	0.04
17. CSM	56.39	7.69	⊥	7.69	∞	125.32
18. Consistency	∞	0.11	⊥	0.11	∞	324.14
19. Insertion Sort	0.03	0.06	0.04	0.06	0.18	0.02
20. Selection Sort	∞	0.21	⊥	0.21	∞	0.33
21. Reset Petri Net	∞	0.02	⊥	⊥	∞	0.01
22. Train	42.24	59.21	⊥	⊥	∞	0.46
	18	22	7	19	11	21

Table 1: Verification times (in seconds) using ALV [19].
`⊥’ means termination with the answer `Unable to verify’
and `∞’ means `No answer’ within 10 minutes.

The experiments show that our specialization method always increases the precision of ALV, that is, for every ALV option used, the number of properties verified increases when considering the specialized systems (columns SpSys) instead of the given, non-specialized systems (columns Sys).

As far as the verification times are concerned, the time in column Sys and the time in column SpSys are of the same order of magnitude in almost all cases. In two examples (Peterson and CSM, with the `default’ option) our method substantially reduces the total verification time. Finally, in the Bounded Buffer example (with options `default’ and `A’) our specialization method significantly increases the verification time. Thus, overall, the increase of precision due to the specialization method we have proposed, does not determine a significant degradation of the time performance.

4 Related Work

The use of constraint logic programs in the area of system verification has been proposed by several authors (see [2,6], and [11] for a survey of early works). Also transformation techniques for constraint logic programs have been shown to be useful for the verification of infinite state systems [8,9,15,17,18]. In the approach presented in this paper, constraint logic programs provide as an intermediate representation of the systems to be verified so that one can easily specialize those systems. To these constraint logic programs we apply a variant of the specialization technique presented in [9]. However, unlike [8,9,15,17,18], the final result of our specialization is not a constraint logic program, but a new reactive system which can be analyzed by using any verification tool for reactive systems specified by linear constraints on the integers. We have used the ALV tool [19] to perform the verification task on the specialized systems (see Section 3), but we could have also used (with minor syntactic modifications) other verification tools, such as TReX [1], FAST [3], and LASH [13]. Thus, one can apply to the specialized systems any of the optimization techniques implemented in those verification tools, such as fixpoint acceleration. We leave it for future research to evaluate the combined use of our specialization technique with other available optimization techniques.

Our specialization method is also related to some techniques for abstract interpretation [5] and, in particular, to those proposed in the field of CLP-based verification of infinite state systems [6,2]. For instance, program specialization makes use of generalization operators [9] which are similar to the widening operators used in abstract interpretation. The main difference between program specialization and abstract interpretation is that, when applied to a given system specification, the former produces an equivalent specification, while the latter produces a more abstract (possibly, finite state) model whose semantics is an approximation of the semantics of the given specification. Moreover, since our specialization method returns a new system specification which is written in the same language of the given specification, after performing specialization one may also apply abstract interpretation techniques for proving system properties. Finding combinations of program specialization and abstract interpretation techniques that are most suitable for the verification of infinite state systems is an interesting issue for future research.

Acknowledgements

This work has been partially supported by PRIN-MIUR and by a joint project between CNR (Italy) and CNRS (France) Verification of Infinite State and Real Time Systems. The last author has been supported by an ERCIM grant during his stay at LORIA-INRIA. Thanks to Laurent Fribourg, John Gallagher, and Michael Leuschel for many stimulating conversations.

References

[1] A. Annichini, A. Bouajjani, and M. Sighireanu. TReX: A tool for reachability analysis of complex systems. In Proc. CAV 2001, LNCS 2102, pages 368-372. Springer, 2001.

[2] G. Banda and J. P. Gallagher. Constraint-based abstract semantics for temporal logic: A direct approach to design and implementation. In Proc. LPAR 2010, LNAI 6355, pages 27-45. Springer, 2010.

[3] S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. FAST: Acceleration from theory to practice. Int. J. on Software Tools for Technology Transfer, 10(5):401-424, 2008.

[4] E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.

[5] P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixpoints. In Proc. POPL’77, pages 238-252. ACM Press, 1977.

[6] G. Delzanno and A. Podelski. Constraint-based deductive model checking. Int. J. on Software Tools for Technology Transfer, 3(3):250-270, 2001.

[7] S. Etalle and M. Gabbrielli. Transformations of CLP modules. Theoretical Computer Science, 166:101-146, 1996.

[8] F. Fioravanti, A. Pettorossi, and M. Proietti. Verifying CTL properties of infinite state systems by specializing constraint logic programs. In Proc. VCL’01, Tech. Rep. DSSE-TR-2001-3, pages 85-96. Univ. of Southampton, UK, 2001.

[9] F. Fioravanti, A. Pettorossi, M. Proietti, and V. Senni. Program specialization for verifying infinite state systems: An experimental evaluation. In Proc. LOPSTR 2010, LNCS 6564, pages 164-183. Springer, 2011.

[10] F. Fioravanti, A. Pettorossi, M. Proietti, and V. Senni. Improving reachability analysis of infinite state systems by specialization. In G. Delzanno and I. Potapov, editors, Proc. Int. Workshop on Reachability Problems (RP 2011), September 28-30, 2011, Genova, Italy, LNCS 6945. Springer, 2011.

[11] L. Fribourg. Constraint logic programming applied to model checking. In Proc. LOPSTR ’99, LNCS 1817, pages 31-42. Springer-Verlag, 2000.

[12] N. D. Jones, C. K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall, 1993.

[13] LASH: http://www.montefiore.ulg.ac.be/~boigelot/research/lash

[14] M. Leuschel and M. Bruynooghe. Logic program specialisation through partial deduction: Control issues. Theory and Practice of Logic Programming, 2(4&5):461-515, 2002.

[15] M. Leuschel and T. Massart. Infinite state model checking by abstract interpretation and program specialization. In Proc. LOPSTR ’99, LNCS 1817, pages 63-82. Springer, 2000.

[16] MAP: http://map.uniroma2.it/mapweb

[17] J. C. Peralta and J. P. Gallagher. Convex hull abstractions in specialization of CLP programs. In Proc. LOPSTR 2002, LNCS 2664, pages 90-108, 2003.

[18] A. Roychoudhury, K. Narayan Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan, and S. A. Smolka. Verification of parameterized systems using logic program transformations. In Proc. TACAS 2000, LNCS 1785, pages 172-187. Springer, 2000.

[19]T. Yavuz-Kahveci and T. Bultan. Action Language Verifier: An infinite-state model checker for reactive software specifications. Formal Methods in System Design, 35(3):325-367, 2009.