Sciweavers

Share
SAS
2000
Springer

A Transformational Approach for Generating Non-linear Invariants

8 years 7 months ago
A Transformational Approach for Generating Non-linear Invariants
Computing invariants is the key issue in the analysis of infinite-state systems whether analysis means testing, verification or parameter synthesis. In particular, methods that allow to treat combinations of loops are of interest. We present a set of algorithms and methods that can be applied to characterize over-approximations of the set of reachable states of combinations of self-loops. We present two families of complementary techniques. The first one identifies a number of basic cases of pair of self-loops for which we provide an exact characterization of the reachable states. The second family of techniques is a set of rules based on static analysis that allow to reduce n self-loops (n 2) to n-1 independent pairs of self-loops. The results of the analysis of the pairs of self-loops can then be combined to provide an over-approximation of the reachable states of the n self-loops. We illustrate our methods by synthesizing conditions under which the Biphase Mark protocol works prope...
Saddek Bensalem, Marius Bozga, Jean-Claude Fernand
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 2000
Where SAS
Authors Saddek Bensalem, Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Yassine Lakhnech
Comments (0)
books