Transformational Verification of Parameterized Protocols Using Array Formulas

  • Alberto Pettorossi
  • Maurizio Proietti
  • Valerio Senni
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3901)


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.


Model Check Logic Program Logic Programming Transformation Rule Critical Section 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Apt, K.R., Bol, R.N.: Logic programming and negation: A survey. Journal of Logic Programming 19(20), 9–71 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Information Processing Letters 22(6), 307–309 (1986)MathSciNetCrossRefGoogle Scholar
  3. 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)CrossRefGoogle Scholar
  4. 4.
    Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. Journal of the ACM 24(1), 44–67 (1977)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)Google Scholar
  6. 6.
    Delzanno, G.: Constraint-based verification of parameterized cache coherence protocols. Formal Methods in System Design 23(3), 257–301 (2003)CrossRefzbMATHGoogle Scholar
  7. 7.
    Delzanno, G., Podelski, A.: Constraint-based deductive model checking. International Journal on Software Tools for Technology Transfer 3(3), 250–270 (2001)zbMATHGoogle Scholar
  8. 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)CrossRefGoogle Scholar
  9. 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. 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)CrossRefGoogle Scholar
  11. 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)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Lamport, L.: A new solution of Dijkstra’s concurrent programming problem. Communications of the ACM 17(8), 453–455 (1974)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 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)CrossRefGoogle Scholar
  14. 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)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 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)CrossRefGoogle Scholar
  16. 16.
    Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer, Berlin (1987)CrossRefzbMATHGoogle Scholar
  17. 17.
    MAP group. The MAP transformation system (1995-2005),
  18. 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)CrossRefGoogle Scholar
  19. 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)CrossRefGoogle Scholar
  20. 20.
    Peterson, G.L.: Myths about the mutual exclusion problem. Information Processing Letters 12(3), 115–116 (1981)CrossRefzbMATHGoogle Scholar
  21. 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)CrossRefGoogle Scholar
  22. 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)CrossRefGoogle Scholar
  23. 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)CrossRefGoogle Scholar
  24. 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)CrossRefGoogle Scholar
  25. 25.
    Seki, H.: Unfold/fold transformation of stratified programs. Theoretical Computer Science 86, 107–139 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Senni, V.: Transformational verification of the parameterized Peterson’s protocol. Unpublished note (July 2005)Google Scholar
  27. 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)CrossRefGoogle Scholar
  28. 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. 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)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Alberto Pettorossi
    • 1
  • Maurizio Proietti
    • 2
  • Valerio Senni
    • 1
  1. 1.DISPUniversity of Roma Tor VergataRomaItaly
  2. 2.IASI-CNRRomaItaly

Personalised recommendations