Hostname: page-component-cd9895bd7-fscjk Total loading time: 0 Render date: 2024-12-23T18:52:45.019Z Has data issue: false hasContentIssue false
  • English
  • Français

Constraint-based automatic verification of abstract models of multithreaded programs

Published online by Cambridge University Press:  01 January 2007

GIORGIO DELZANNO
GIORGIO DELZANNO*
Affiliation:
Dipartimento di Informatica e Scienze dell'Informazione, Università di Genova, via Dodecaneso 35, 16146 Genova, Italy (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

We present a technique for the automated verification of abstract models of multithreaded programs providing fresh name generation, name mobility, and unbounded control. As high level specification language we adopt here an extension of communication finite-state machines with local variables ranging over an infinite name domain, called TDL programs. Communication machines have been proved very effective for representing communication protocols as well as for representing abstractions of multithreaded software. The verification method that we propose is based on the encoding of TDL programs into a low level language based on multiset rewriting and constraints that can be viewed as an extension of Petri Nets. By means of this encoding, the symbolic verification procedure developed for the low level language in our previous work can now be applied to TDL programs. Furthermore, the encoding allows us to isolate a decidable class of verification problems for TDL programs that still provide fresh name generation, name mobility, and unbounded control. Our syntactic restrictions are in fact defined on the internal structure of threads: In order to obtain a complete and terminating method, threads are only allowed to have at most one local variable (ranging over an infinite domain of names).

Keywords

constraintsmultithreaded programsverification
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 7 , Issue 1-2 , January 2007 , pp. 67 - 91
Copyright
Copyright © Cambridge University Press 2007

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abdulla, P. A., Cerāns, K., Jonsson, B., and Tsay, Y.-K. 1996. General Decidability Theorems for Infinite-State Systems. In Proceedings 11th Annual International Symposium on Logic in Computer Science (LICS'96). IEEE Computer Society Press, New Brunswick, New Jersey, 313–321.Google Scholar
Abdulla, P. A. and Jonsson, B. 2001. Ensuring Completeness of Symbolic Verification Methods for Infinite-State Systems. Theoretical Computer Science 256, 1-2, 145–167.CrossRefGoogle Scholar
Abdulla, P. A. and Jonsson, B. 2003. Model checking of systems with many identical timed processes. Theoretical Computer Science 290, 1, 241–264.CrossRefGoogle Scholar
Abdulla, P. A. and Nylén, A. 2000. Better is Better than Well: On Efficient Verification of Infinite-State Systems. In Proceedings 15th Annual International Symposium on Logic in Computer Science (LICS'00). IEEE Computer Society Press, Santa Barbara, California, 132–140.Google Scholar
Ball, T., Chaki, S., and Rajamani, S. K. 2001. Parameterized Verification of Multithreaded Software Libraries. In 7th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2001), Genova, Italy, April 2-6,. LNCS, vol. 2031. Springer-Verlag, 158–173.Google Scholar
Bistarelli, S., Cervesato, I., Lenzini, G., and Martinelli, F. 2005. Relating multiset rewriting and process algebras for security protocol analysis. Journal of Computer Security 13, 1, 3–47.CrossRefGoogle Scholar
Bochmann, G. V. 1978. Finite state descriptions of communicating protocols. Computer Networks 2, 46–57.Google Scholar
Bouajjani, A., Jonsson, B., Nilsson, M., and Touili, T. 2000. Regular Model Checking. In Proceedings 12th International Conference on Computer Aided Verification (CAV'00), Emerson, E. A. and Sistla, A. P., Eds. LNCS, vol. 1855. Springer-Verlag, Chicago, Illinois, 403–418.Google Scholar
Bozzano, M. and Delzanno, G. 2002. Algorithmic verification of invalidation-based protocols. In 14th International Conference on Computer Aided Verification, CAV'02. Lecture Notes in Computer Science, vol. 2404. Springer.Google Scholar
Cervesato, I., Durgin, N., Lincoln, P., Mitchell, J., and Scedrov, A. 1999. A Meta-notation for Protocol Analysis. In 12th Computer Security Foundations Workshop (CSFW'99). IEEE Computer Society Press, Mordano, Italy, 55–69.Google Scholar
Delzanno, G. 2001. An Assertional Language for Systems Parametric in Several Dimensions. In Verification of Parameterized Systems – VEPAS 2001. ENTCS, vol. 50.Google Scholar
Delzanno, G. 2005. Constraint Multiset Rewriting. Tech. Rep. TR-05-08, Dipartimento Informatica e Scienze dell'Informazione, Università di Genova, Italia.Google Scholar
Delzanno, G. and Podelski, A. 1999. Model checking in CLP. In Proceedings 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'99). Lecture Notes in Computer Science, vol. 1579. Springer-Verlag, Amsterdam, The Netherlands, 223–239.Google Scholar
Finkel, A. and Schnoebelen, P. 2001. Well-Structured Transition Systems Everywhere! Theoretical Computer Science 256, 1-2, 63–92.CrossRefGoogle Scholar
German, S. M. and Sistla, A. P. 1992. Reasoning about Systems with Many Processes. Journal of the ACM 39, 3, 675–735.CrossRefGoogle Scholar
Gordon, A. D. 2001. Notes on nominal calculi for security and mobility. In Foundations of Security Analysis and Design, Tutorial Lectures. Lecture Notes in Computer Science, vol. 2171. Springer, 262–330.CrossRefGoogle Scholar
Kesten, Y., Maler, O., Marcus, M., Pnueli, A., and Shahar, E. 2001. Symbolic model checking with rich assertional languages. Theoretical Computer Science 256, 1, 93–112.CrossRefGoogle Scholar
Schnoebelen, P. 2002. Verifying Lossy Channel Systems has Nonprimitive Recursive Complexity. Information Processing Letters 83, 5, 251–261.CrossRefGoogle Scholar