Behavioral Automata Composition for Automatic Topology Independent Verification of Parameterized Systems







Deposit Papers 


Hanna, Youssef, Basu, Samik and Rajan, Hridesh (2009) Behavioral Automata Composition for Automatic Topology Independent Verification of Parameterized Systems. Technical Report 09-17, Computer Science, Iowa State University.

Full text available as:Adobe PDF

There is a later version of this eprint available: Click here to view it.


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 get 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 that presented in the existing literature.

Subjects:Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
Software: PROGRAMMING LANGUAGES: Formal Definitions and Theory (D.2.1, F.3.1-2, F.4.2-3)
ID code:00000597
Deposited by:Youssef Hanna on 20 March 2009

Available Versions of This Paper

Contact site administrator at: