Abstract
We consider infinite state reactive systems specified by using linear constraints over the integers, and we address the problem of verifying safety properties of these systems by applying reachability analysis techniques. We propose a method based on program specialization, which improves the effectiveness of the backward and forward reachability analyses. For backward reachability our method consists in: (i) specializing the reactive system with respect to the initial states, and then (ii) applying to the specialized system a reachability analysis that works backwards from the unsafe states. For forward reachability our method works as for backward reachability, except that the role of the initial states and the unsafe states are interchanged. We have implemented our method using the MAP transformation system and the ALV verification system. Through various experiments performed on several infinite state systems, we have shown that our specialization-based verification technique considerably increases the number of successful verifications without significantly degrading the time performance.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abdulla, P.A., Delzanno, G., Ben Henda, N., Rezine, A.: Monotonic abstraction (On efficient verification of parameterized systems). Int. J. of Foundations of Computer Science 20(5), 779–801 (2009)
Annichini, A., Bouajjani, A., Sighireanu, M.: TReX: A tool for reachability analysis of complex systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 368–372. Springer, Heidelberg (2001)
Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: Acceleration from theory to practice. Int. J. on Software Tools for Technology Transfer 10(5), 401–424 (2008)
Bultan, T., Gerber, R., Pugh, W.: Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results. ACM TOPLAS 21(4), 747–789 (1999)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixpoints. In: Proc. POPL 1977, pp. 238–252. ACM Press, New York (1977)
Dams, D., Grumberg, O., Gerth, R.: Abstract interpretation of reactive systems. ACM TOPLAS 19(2), 253–291 (1997)
Delzanno, G.: Constraint-based verification of parameterized cache coherence protocols. Formal Methods in System Design 23(3), 257–301 (2003)
Delzanno, G., Podelski, A.: Constraint-based deductive model checking. Int. J. on Software Tools for Technology Transfer 3(3), 250–270 (2001)
Esparza, J.: Decidability of model checking for infinite-state concurrent systems. Acta Informatica 34(2), 85–107 (1997)
Etalle, S., Gabbrielli, M.: Transformations of CLP modules. Theoretical Computer Science 166, 101–146 (1996)
Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying CTL properties of infinite state systems by specializing constraint logic programs. In: Proc. VCL 2001, Tech. Rep. DSSE-TR-2001-3, pp. 85–96. Univ. of Southampton, UK (2001)
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Program specialization for verifying infinite state systems: An experimental evaluation. In: Alpuente, M. (ed.) LOPSTR 2010. LNCS, vol. 6564, pp. 164–183. Springer, Heidelberg (2011)
Frehse, G.: PHAVer: Algorithmic verification of hybrid systems past HYTECH. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258–273. Springer, Heidelberg (2005)
Fribourg, L.: Constraint logic programming applied to model checking. In: Bossi, A. (ed.) LOPSTR 1999. LNCS, vol. 1817, pp. 31–42. Springer, Heidelberg (2000)
Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 426–440. Springer, Heidelberg (2001)
Henzinger, T.A.: The theory of hybrid automata. In: Proc., LICS 1996, pp. 278–292 (1996)
Jaffar, J., Maher, M.: Constraint logic programming: A survey. J. of Logic Programming 19/20, 503–581 (1994)
Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice Hall, Englewood Cliffs (1993)
LASH homepage, http://www.montefiore.ulg.ac.be/~boigelot/research/lash
Leuschel, M., Massart, T.: Infinite state model checking by abstract interpretation and program specialization. In: Bossi, A. (ed.) LOPSTR 1999. LNCS, vol. 1817, pp. 63–82. Springer, Heidelberg (2000)
MAP homepage, http://www.iasi.cnr.it/~proietti/system.html
Peralta, J.C., Gallagher, J.P.: Convex hull abstractions in specialization of CLP programs. In: Leuschel, M. (ed.) LOPSTR 2002. LNCS, vol. 2664, pp. 90–108. Springer, Heidelberg (2003)
Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A.: Verification of parameterized systems using logic program transformations. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, pp. 172–187. Springer, Heidelberg (2000)
Yavuz-Kahveci, T., Bultan, T.: Action Language Verifier: An infinite-state model checker for reactive software specifications. Formal Methods in System Design 35(3), 325–367 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V. (2011). Improving Reachability Analysis of Infinite State Systems by Specialization. In: Delzanno, G., Potapov, I. (eds) Reachability Problems. RP 2011. Lecture Notes in Computer Science, vol 6945. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24288-5_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-24288-5_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24287-8
Online ISBN: 978-3-642-24288-5
eBook Packages: Computer ScienceComputer Science (R0)