Behavioral automata composition for automatic topology independent verification of parameterized systems

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Behavioral automata composition for automatic topology independent verification of parameterized systems

Full text

Pdf (726 KB)

Source

Foundations of Software Engineering archive
Proceedings of the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering on European software engineering conference and foundations of software engineering symposium table of contents

Amsterdam, The Netherlands

SESSION: Specification and verification 2 table of contents

Pages 325-334

Year of Publication: 2009

ISBN:978-1-60558-001-2

Authors

Youssef Hanna	Iowa State University, Ames, IA, USA
Samik Basu	Iowa State University, Ames, IA, USA
Hridesh Rajan	Iowa State University, Ames, IA, USA

Sponsors

ACM: Association for Computing Machinery
SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 11, Downloads (12 Months): 25, Citation Count: 0

Additional Information:

abstract references index terms

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1595696.1595758 What is a DOI?

ABSTRACT

Verifying correctness properties of parameterized systems is a long-standing problem. The challenge lies in the lack of guarantee that the property is satisfied for all instances of the parameterized system. Existing work on addressing this challenge aims to reduce this problem to checking the properties on smaller systems with a bound on the parameter referred to as the cut-off. A property satisfied on the system with the cut-off ensures that it is satisfied for systems with any larger parameter. The major problem with these techniques is that they only work for certain classes of systems with specific communication topology such as ring topology, thus leaving other interesting classes of systems unverified. We contribute an automated technique for finding the cut-off of the parameterized system that works for systems defined with any topology. Given the specification and the topology of the system, our technique is able to automatically generate the cut-off specific to this system. We prove the soundness of our technique and demonstrate its effectiveness and practicality by applying it to several canonical examples where in some cases, our technique obtains smaller cut-off values than those presented in the existing literature.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	P. A. Abdulla, G. Delzanno, N. B. Henda, and A. Rezine. Regular model checking without transducers (on efficient verification of parameterized systems). In TACAS, pages 721-736, 2007.
	2	P. A. Abdulla, B. Jonsson, M. Nilsson, and J. d'Orso. Regular model checking made simple and efficient. In CONCUR, pages 116--130, 2002.
	3	T. E. Anderson. The performance of spin lock alternatives for shared-memory multiprocessors. IEEE Trans. Parallel Distrib. Syst., 1(1):6--16, 1990.
	4	K. R. Apt and D. C. Kozen. Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett., 22(6):307--309, 1986.
	5	T. Arons, A. Pnueli, S. Ruah, J. Xu, and L. D. Zuck. Parameterized verification with automatically computed inductive assertions. In CAV, pages 221--234, 2001.
	6	P. Baldan, A. Corradini, and B. König. A framework for the verification of infinite-state graph transformation systems. Inf. Comput., 206(7):869--907, 2008.
	7	P. Baldan, B. König, and A. Rensink. Graph grammar verification through abstraction. In Dagstuhl Seminar Proceedings 04241, 2005.
	8	T. Ball, S. Chaki, and S. K. Rajamani. Parameterized verification of multithreaded software libraries. In TACAS, pages 158--173, 2001.
	9	S. Basu and C. R. Ramakrishnan. Compositional analysis for verification of parameterized systems. Theor. Comput. Sci., 354(2):211--229, 2006.
	10	A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular model checking. In CAV, pages 403--418, 2000.
	11	A. Bouajjani, Y. Jurski, and M. Sighireanu. Reasoning about dynamic networks of infinite-state processes with global synchronization. HAL - CCSD, 2006.
	12	A. Bouajjani, Y. Jurski, and M. Sighireanu. A generic framework for reasoning about dynamic networks of infinite-state processes. In TACAS, pages 690--705, 2007.
	13	E. Clarke, M. Talupur, and H. Veith. Environment abstraction for parameterized verification. In VMCAI, 126--141, 2006.
	14	E. M. Clarke, O. Grumberg, and S. Jha. Verifying parameterized networks using abstraction and regular languages. In CONCUR, pages 395--407, 1995.
	15	E. M. Clarke, M. Talupur, and H. Veith. Proving ptolemy right: The environment abstraction framework for model checking concurrent systems. In TACAS, pages 33--47, 2008.
	16	E. Dijkstra. Two starvation free solutions to a general exclusion problem. EWD 625, Plataanstraat 5, 5671 AL Neunen, The Netherlands.
	17	E. A. Emerson and V. Kahlon. Model checking large-scale and parameterized resource allocation systems. In TACAS, pages 251--265, 2002.
	18	E. A. Emerson and V. Kahlon. Exact and efficient verification of parameterized cache coherence protocols. In CHARME, pages 247--262, 2003.
	19	E. A. Emerson and K. S. Namjoshi. Reasoning about rings. In POPL, pages 85--94, 1995.
	20	E. A. Emerson and K. S. Namjoshi. Automatic verification of parameterized synchronous systems (extended abstract). In CAV, pages 87--98, 1996.
	21	E. A. Emerson, R. J. Trefler, and T. Wahl. Reducing model checking of the few to the one. In ICFEM, pp. 94--113, 2006.
	22	D. Fisman, O. Kupferman, and Y. Lustig. On verifying fault tolerance of distributed protocols. In TACAS, 315-331, 2008.
	23	S. M. German and A. P. Sistla. Reasoning about systems with many processes. J. ACM, 39(3):675--735, 1992.
	24	Y. Hanna, S. Basu, and H. Rajan. Behavioral automata composition for automatic topology independent verification of parameterized systems. Technical Report 09-17, Computer Sc., Iowa State U., 2009.
	25	C. N. Ip and D. L. Dill. Verifying systems with replicated components in murphi. In CAV, pages 147--158, 1996.
	26	M. Llorens and J. Oliver. Introducing structural dynamic changes in petri nets: Marked-controlled reconfigurable nets. In ATVA, pages 310--323, 2004.
	27	R. Milner. A Calculus of Communicating Systems. Springer-Verlag New York, Inc., 1982.
	28	A. Pnueli, S. Ruah, and L. D. Zuck. Automatic deductive verification with invisible invariants. In TACAS '01, 92--97.
	29	A. Pnueli, J. Xu, and L. D. Zuck. Liveness with (0, 1, infty)-counter abstraction. In CAV, pp. 107--122, 2002.
	30	M. Saksena, O. Wibling, and B. Jonsson. Graph grammar modeling and verification of ad hoc routing protocols. In TACAS, pages 18--32, 2008.
	31	P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In the International Workshop on Automatic Verification Methods for Finite State Systems, pages 68--80, 1990.