Improving Reachability Analysis of Infinite State Systems by Specialization

• Autorzy: Fioravanti F. , Pettorossi A. , Proietti M. , Senni V.
• Języki publikacji: EN

Abstrakty

EN

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 the reachability analysis that works backwards from the unsafe states. For reasons of efficiency, during specialization we make use of a relaxation from integers to reals. In particular, we test the satisfiability or entailment of constraints over the real numbers, while preserving the reachability properties of the reactive systems when constraints are interpreted over the integers. 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 a significant degradation of the time performance.

Słowa kluczowe

EN

reachability analysis; automatic verification; program transformation; constraint logic programming (CLP)

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2012
• Tom: Vol. 119, nr 3/4
• Strony: 281--300
• Opis fizyczny: Bibliogr. 40 poz., tab.

Twórcy

autor

Fioravanti F.

autor

Pettorossi A.

autor

Proietti M.

autor

Senni V.

• Department of Sciences, University of Chieti-Pescara, Viale Pindaro 42, 65127 Pescara, Italy,

Bibliografia

• [1] P. A. Abdulla, G. Delzanno, N. Ben Henda, and A. Rezine. Monotonic abstraction (On efficient verification of parameterized systems). International Journal of Foundations of Computer Science, 20(5):779-801, 2009.
• [2] A. Annichini, A. Bouajjani, and M. Sighireanu. TReX: A tool for reachability analysis of complex systems. In G. Berry, H. Comon, and A. Finkel, editors, Proceedings of the 13th International Conference on Computer Aided Verification, CAV 2001, Paris, France, July 18-22, 2001, Lecture Notes in Computer Science 2102, pages 368-372. Springer, 2001.
• [3] R. Bagnara, P. M. Hill, and E. Zaffanella. The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming, 72(1-2):3-21, 2008.
• [4] S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. FAST: Acceleration from theory to practice. International Journal on Software Tools for Technology Transfer, 10(5):401-424, 2008.
• [5] B. Bérard and L. Fribourg. Reachability analysis of (timed) Petri nets using real arithmetic. In Proceedings of CONCUR '99: Concurrency Theory, 10th International Conference, Eindhoven, The Netherlands, August 24-27, 1999, Lecture Notes in Computer Science 1664, pages 178-193. Springer, 1999.
• [6] T. Bultan, R. Gerber, and W. Pugh. Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results. ACM Transactions on Programming Languages and Systems, 21(4):747-789, 1999.
• [7] E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
• [8] P. Cousot. Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes (in French). Th`ese d' ´ Etat `es sciences mathématiques, Université Joseph Fourier, Grenoble, France, 21 March 1978.
• [9] P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixpoints. In Proceedings of the 4th ACM-SIGPLAN Symposium on Principles of Programming Languages, POPL '77, pages 238-252. ACM Press, 1977.
• [10] P. Cousot, P. Ganty, and J.-F. Raskin. Fixpoint-guided abstraction refinements. In G. Filé and H. Riis Nielson, editors, Proceedings of the Fourteenth International Symposium on Static Analysis, SAS '07, Kongens Lyngby, Denmark, Lecture Notes in Computer Science 4634, pages 333-348. Springer, 22-24 August 2007.
• [11] P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proceedings of the Fifth ACM Symposium on Principles of Programming Languages, POPL '78, pages 84-96. ACM Press, 1978.
• [12] D. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems, 19(2):253-291, 1997.
• [13] G. Delzanno. Constraint-based verification of parameterized cache coherence protocols. Formal Methods in System Design, 23(3):257-301, 2003.
• [14] G. Delzanno and A. Podelski. Constraint-based deductive model checking. International Journal on Software Tools for Technology Transfer, 3(3):250-270, 2001.
• [15] J. Esparza. Decidability of model checking for infinite-state concurrent systems. Acta Informatica, 34(2):85-107, 1997.
• [16] S. Etalle and M. Gabbrielli. Transformations of CLP modules. Theoretical Computer Science, 166:101-146, 1996.
• [17] F. Fioravanti. Transformation of Constraint Logic Programs for Software Specialization and Verification. PhD thesis, Universit`a di Roma "La Sapienza", Italy, 2002.
• [18] F. Fioravanti, A. Pettorossi, and M. Proietti. Verifying CTL properties of infinite state systems by specializing constraint logic programs. In Proceedings of the ACM SIGPLAN Workshop on Verification and Computational Logic VCL'01, Florence (Italy), Technical Report DSSE-TR-2001-3, pages 85-96. University of Southampton, UK, 2001.
• [19] F. Fioravanti, A. Pettorossi, and M. Proietti. Transformation rules for locally stratified constraint logic programs. In K.-K. Lau and M. Bruynooghe, editors, Program Development in Computational Logic, Lecture Notes in Computer Science 3049, pages 292-340. Springer-Verlag, 2004.
• [20] F. Fioravanti, A. Pettorossi, M. Proietti, and V. Senni. Controlling polyvariance for specialization-based verification. In Proceedings of the 26th Italian Conference on Computational Logic, CILC 2011, 31 August - 2 September 2011, Pescara, Italy, volume 810 urn:nbn:de:0074-810-0, pages 179-197. CEUR-WS, 2011.
• [21] 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, Proceedings of the 5th International Workshop on Reachability Problems, RP 2011, September 28-30, 2011, Genova, Italy, Lecture Notes in Computer Science 6945, pages 165-179. Springer, 2011.
• [22] F. Fioravanti, A. Pettorossi, M. Proietti, and V. Senni. Generalization strategies for the verification of infinite state systems. Theory and Practice of Logic Programming. Available on CJO 2012 doi:10.1017/S1471068411000627. Special Issue on the 25th GULP Annual Conference, 2012.
• [23] G. Frehse. PHAVer: Algorithmic verification of hybrid systems past HyTech. In M. Morari and L. Thiele, editors, Hybrid Systems: Computation and Control, 8th International Workshop, HSCC 2005, Lecture Notes in Computer Science 3414, pages 258-273. Springer, 2005.
• [24] L. Fribourg. Constraint logic programming applied to model checking. In A. Bossi, editor, Proceedings of the 9th International Workshop on Logic-based Program Synthesis and Transformation, LOPSTR '99, Venezia, Italy, Lecture Notes in Computer Science 1817, pages 31-42. Springer-Verlag, 2000.
• [25] P. Godefroid, M. Huth, and R. Jagadeesan. Abstraction-based model checking using modal transition systems. In Proceedings of CONCUR '01, Lecture Notes in Computer Science 2154, pages 426-440. Springer, 2001.
• [26] T. A. Henzinger. The theory of hybrid automata. In 11th IEEE Symposium on Logic in Computer Science, LICS '96, pages 278-292, 1996.
• [27] J. Jaffar and M. Maher. Constraint logic programming: A survey. Journal of Logic Programming, 19/20:503-581, 1994.
• [28] R. Jhala and R. Majumdar. Software model checking. ACM Comput. Surv., 41(4):21:1-21:54, October 2009.
• [29] N. D. Jones, C. K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall, 1993.
• [30] LASH. homepage: http://www.montefiore.ulg.ac.be/∼boigelot/research/lash.
• [31] M. Leuschel and T. Massart. Infinite state model checking by abstract interpretation and program specialization. In A. Bossi, editor, Proceedings of the 9th International Workshop on Logic-based Program Synthesis and Transformation, LOPSTR '99, Venezia, Italy, Lecture Notes in Computer Science 1817, pages 63-82. Springer, 2000.
• [32] MAP. The MAP transformation system. Available from: http://www.iasi.cnr.it/∼proietti/system.html, 1995-2010.
• [33] J. Midtgaard. Control-flow analysis of functional programs. ACM Computing Surveys, 2012. Forthcoming.
• [34] H. R. Nielson, F. Nielson, and C. Hankin. Principles of Program Analysis. Springer, 1999.
• [35] J. C. Peralta and J. P. Gallagher. Convex hull abstractions in specialization of CLP programs. In M. Leuschel, editor, Logic Based Program Synthesis and Tranformation, 12th International Workshop, LOPSTR 2002, Madrid, Spain, September 17-20, 2002, Revised Selected Papers, Lecture Notes in Computer Science 2664, pages 90-108, 2003.
• [36] F. Ranzato, O. Rossi Doria, and F. Tapparo. A forward-backward abstraction refinement algorithm. In F. Logozzo, D. A. Peled, and L. D. Zuck, editors, Proceedings 9th International Conference on Verification, Model Checking and Abstract Interpretation, VMCAI '08, San Francisco, CA, USA, Lecture Notes in Computer Science 4905, pages 248-262. Springer, 2008.
• [37] A. Roychoudhury, K. Narayan Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan, and S. A. Smolka. Verification of parameterized systems using logic program transformations. In Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000, Berlin, Germany, Lecture Notes in Computer Science 1785, pages 172-187. Springer, 2000.
• [38] A. Schrijver. Theory of Linear and Integer Programming. John Wiley & Sons, 1986.
• [39] H. Seki. On negative unfolding in the answer set semantics. In M. Hanus, editor, Logic-Based Program Synthesis and Transformation, 18th International Symposium, LOPSTR 2008, Valencia, Spain, July 17-18,
• [40] 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.