Behavioral Automata Composition for Automatic Topology Independent Verification of Parameterized Systems

By: Youssef Hanna, Samik Basu, and Hridesh Rajan

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.

Other Info

ACM Reference

Hanna, Y. et al. 2009. Behavioral Automata Composition for Automatic Topology Independent Verification of Parameterized Systems. Proceedings of the 7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, Amsterdam, The Netherlands (2009), 325–334.

BibTeX Reference

@inproceedings{HannaBasuRajan2009a,
  author = {Youssef Hanna and Samik Basu and Hridesh Rajan},
  title = {Behavioral Automata Composition for Automatic Topology Independent Verification of Parameterized Systems},
  booktitle = {Proceedings of the 7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, Amsterdam, The Netherlands},
  pages = {325--334},
  year = {2009},
  publisher = {{ACM}},
  editor = {Hans van Vliet and Val{\'{e}}rie Issarny},
  doi = {10.1145/1595696.1595758},
  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.},
}