Next: Development/Integration of tools and
Up: Work progress and achievements
Previous: Verification methods and techniques
Several works in our project show how to combine complementary analysis techniques
in order to tackle complex validation problems.
- static analysis techniques such as slicing techniques and live variable
analysis are used to generate reduced models (finite-state or extended automata)
which are analyzed using model-checking algorithms or
symbolic reachability analysis procedures.
- abstraction techniques are used to generate automatically
(abstract) extended automata which can be analyzed using
model-checking algorithms or symbolic reachability analysis techniques.
- conversely, symbolic reachability analysis procedures for infinite-state systems
are used to generate automatically finite-state abstract models
which are analyzed using model-checking algorithms.
This approach was applied to the analysis of protocols
with complex relations between their variables and parameters.
- abstraction techniques and finite-state model-checking are used in
deriving candidate induction assertions, and to prove
that the candidate assertions are indeed inductive.
This methodology has been applied to the verification
of nontrivial parametrized systems such as mutual
exclusion protocols and cache coherence protocols.