Transformational Verification of Parameterized Protocols Using Array Formulas | SpringerLink
Skip to main content
Springer Nature Link
Log in

Transformational Verification of Parameterized Protocols Using Array Formulas

  • Conference paper
Logic Based Program Synthesis and Transformation (LOPSTR 2005)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3901))

  • 224 Accesses

Abstract

We propose a method for the specification and the automated verification of temporal properties of parameterized protocols. Our method is based on logic programming and program transformation. We specify the properties of parameterized protocols by using an extension of stratified logic programs. This extension allows premises of clauses to contain first order formulas over arrays of parameterized length. A property of a given protocol is proved by applying suitable unfold/fold transformations to the specification of that protocol. We demonstrate our method by proving that the parameterized Peterson’s protocol among N processes, for any N ≥ 2, ensures the mutual exclusion property.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Apt, K.R., Bol, R.N.: Logic programming and negation: A survey. Journal of Logic Programming 19(20), 9–71 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  2. Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Information Processing Letters 22(6), 307–309 (1986)

    Article  MathSciNet  Google Scholar 

  3. Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized Verification with Automatically Computed Inductive Assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 221–234. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  4. Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. Journal of the ACM 24(1), 44–67 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  5. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)

    Google Scholar 

  6. Delzanno, G.: Constraint-based verification of parameterized cache coherence protocols. Formal Methods in System Design 23(3), 257–301 (2003)

    Article  MATH  Google Scholar 

  7. Delzanno, G., Podelski, A.: Constraint-based deductive model checking. International Journal on Software Tools for Technology Transfer 3(3), 250–270 (2001)

    MATH  Google Scholar 

  8. Fioravanti, F., Pettorossi, A., Proietti, M.: Automated strategies for specializing constraint logic programs. In: Lau, K.-K. (ed.) LOPSTR 2000. LNCS, vol. 2042, pp. 125–146. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  9. Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying CTL properties of infinite state systems by specializing constraint logic programs. In: Proceedings of VCL 2001, Florence, Italy, DSSE-TR-2001-3, pp. 85–96. Univ. of Southampton, UK (2001)

    Google Scholar 

  10. Fioravanti, F., Pettorossi, A., Proietti, M.: Verification of sets of infinite state systems using program transformation. In: Pettorossi, A. (ed.) LOPSTR 2001. LNCS, vol. 2372, pp. 111–128. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  11. Fribourg, L., Olsén, H.: A decompositional approach for computing least fixed-points of Datalog programs with Z-counters. Constraints 2(3/4), 305–335 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  12. Lamport, L.: A new solution of Dijkstra’s concurrent programming problem. Communications of the ACM 17(8), 453–455 (1974)

    Article  MathSciNet  MATH  Google Scholar 

  13. Lazic, R., Newcomb, T.C., Roscoe, A.W.: On model checking data-independent systems with arrays with whole-array operations. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) Communicating Sequential Processes. LNCS, vol. 3525, pp. 275–291. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  15. 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)

    Chapter  Google Scholar 

  16. Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer, Berlin (1987)

    Book  MATH  Google Scholar 

  17. MAP group. The MAP transformation system (1995-2005), http://www.iasi.rm.cnr.it/~proietti/system.html

  18. McMillan, K.L., Qadeer, S., Saxe, J.B.: Induction in compositional model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 312–327. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  19. Nilsson, U., Lübcke, J.: Constraint logic programming for local and symbolic model-checking. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 384–398. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  20. Peterson, G.L.: Myths about the mutual exclusion problem. Information Processing Letters 12(3), 115–116 (1981)

    Article  MATH  Google Scholar 

  21. Pettorossi, A., Proietti, M.: Perfect model checking via unfold/fold transformations. In: Lloyd, J.W. (ed.) CL 2000. LNCS (LNAI), vol. 1861, pp. 613–628. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  22. Ramakrishna, Y.S., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Swift, T., Warren, D.S.: Efficient model checking using tabled resolution. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 143–154. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  23. Roychoudhury, A., Ramakrishnan, I.V.: Automated inductive verification of parameterized protocols. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 25–37. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  24. Roychoudhury, A., Ramakrishnan, C.R.: Unfold/fold transformations for automated verification. In: Bruynooghe, M., Lau, K.-K. (eds.) Program Development in Computational Logic. LNCS, vol. 3049, pp. 261–290. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  25. Seki, H.: Unfold/fold transformation of stratified programs. Theoretical Computer Science 86, 107–139 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  26. Senni, V.: Transformational verification of the parameterized Peterson’s protocol. Unpublished note (July 2005)

    Google Scholar 

  27. Shankar, N.: Combining theorem proving and model checking through symbolic analysis. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 1–16. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  28. Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: LICS 2001, pp. 29–37. IEEE Press, Los Alamitos (2001)

    Google Scholar 

  29. Zuck, L.D., Pnueli, A.: Model checking and abstraction to the aid of parameterized systems (a survey). Computer Languages, Systems & Structures 30(3-4), 139–169 (2004)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DISP, University of Roma Tor Vergata, Via del Politecnico 1, I-00133, Roma, Italy

    Alberto Pettorossi & Valerio Senni

  2. IASI-CNR, Viale Manzoni 30, I-00185, Roma, Italy

    Maurizio Proietti

Authors
  1. Alberto Pettorossi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Maurizio Proietti
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Valerio Senni
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing, University of Leeds, UK

    Patricia M. Hill

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pettorossi, A., Proietti, M., Senni, V. (2006). Transformational Verification of Parameterized Protocols Using Array Formulas. In: Hill, P.M. (eds) Logic Based Program Synthesis and Transformation. LOPSTR 2005. Lecture Notes in Computer Science, vol 3901. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11680093_3

Download citation

  • DOI: https://doi.org/10.1007/11680093_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-32654-0

  • Online ISBN: 978-3-540-32656-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation