Approximated Context-Sensitive Analysis for Parameterized Verification
Parosh Aziz Abdulla, Giorgio Delzanno, Ahmed Rezine
We propose a verification method for parameterized systems with global conditions. The method is based on context-sensitive constraints, a symbolic representation of infinite sets of configurations defined on top of words over a finite alphabet. We first define context-sensitive constraints for an exact symbolic backward analysis of parameterized systems with global conditions. Since the model is Turing complete, such an analysis is not guaranteed to terminate. To turn the method into a verification algorithm, we introduce context-sensitive constraints that over-approximate the set of backward reachable states and show how to symbolically test entailment and compute predecessors. We apply the resulting algorithm to automatically verify parameterized models for which the exact analysis and other existing verification methods either diverge or return false positives.
In Proceedings of the 11th Formal Methods for Open Object-Based Distributed Systems and 29th Formal Techniques for Networked and Distributed Systems (FMOODS/FORTE), 2009,
Last version (pdf) 2009