Supervisor

Suitable for

Abstract

Many systems are built from some number N of similar components; a common verification problem is to verify such systems for all values of the system size N. Clearly one cannot perform such a verification directly using a model checker such as FDR.

I recently proposed an approach to this problem [1]. The idea is to build a process that:

• is an abstraction of the system in question; and
• meets the required specification,

for all possible system sizes, and for all possible values of the underlying types.

The abstraction is formed via an iterative approach: the abstraction is guessed, and the model checker used to test whether it is suitable for small values of the system size and the types; if not, the counterexample returned by the model checker is used to improve the guess. Once a suitable abstraction has been found that works for small values of the system size and types, techniques from data independence are used to generalise the result to all such values.

This technique has been applied to verify a well-known security protocol in a system with arbitrarily many honest agents. A paper describing this technique in more detail is available on request.

The aim of this project would be to assess the generality of this approach, by using it to analyse more examples, for example common distributed algorithms, such as those described in [2].

The Concurrency course would be a prerequisite.

References

• [1] Gavin Lowe, On the Application of Counterexample-Guided Abstraction Refinement and Data Independence to the Parameterised Model Checking Problem. In Proceedings of AVIS'04 --- Third International Workshop on Automatic Verification of Infinite-State Systems, 2004.
• [2] Nancy Lynch, Distributed Algorithms, Morgan Kaufmann, 1996.