Title

Behavioral automata composition for automatic topology independent verification of parameterized systems

Campus Units

Computer Science

Document Type

Conference Proceeding

Conference

Proceedings of the the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering (ESEC/FSE '09)

Publication Version

Submitted Manuscript

Link to Published Version

https://doi.org/10.1145/1595696.1595758

Publication Date

2009

Journal or Book Title

Proceedings of the the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering (ESEC/FSE '09)

First Page

325

Last Page

334

DOI

10.1145/1595696.1595758

Conference Date

August 24-28, 2009

City

Amsterdam, The Netherlands

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.

Comments

This is a manuscript of a proceeding published as Hanna, Youssef, Samik Basu, and Hridesh Rajan. "Behavioral automata composition for automatic topology independent verification of parameterized systems." In Proceedings of the the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, pp. 325-334. ACM, 2009. 10.1145/1595696.1595758. Posted with permission.

Rights

© ACM, 2009 This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proceedings of the the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, pp. 325-334. ACM, 2009. https://doi.org/10.1145/1595696.1595758

Copyright Owner

ACM

Language

en

File Format

application/pdf

Published Version

Share

Article Location

 
COinS