Using abstractions to model and verify distributed systems used in cellular telephone networks

Abstract This thesis shows the work performed in with the telecom manufacturer Nortel Networks, my phd advisor was Paul Gastin. It shows how a new protocol was designed as well as how some formal methods were improved. The protocol takes place in a distributed environment with real time and high availability constraints.

The work all started out with the verication of a protocol in charge of the coherency of applications within the distributed system. We have been implementing methods to be able to verify the protocol. These methods are generic and can be reused with other distributed systems.

We have been performing an abstraction on timestamps by introducing objects which ensure the same property of ordering. This type of abstraction can even sometimes change an infinite system into a finite one. We have been implementing this feature within the Spin model checker. This abstraction proved to be useful because is allowed us to check the protocol and find errors in it.

Because of this first verification, we have been designing a new protocol, much simpler. Since the procotol was simpler a more in depth model was created. But there was too many states. We performed an abstraction based of the symmetry of processes. We have been adding two key words to the Spin model checker. These key words allow to use processes addresses while exploiting symmetry of the system. This abstraction made it possible to verify the new protocol.

Download the thesis (1.7 Mo). Only chapter 4 is in english.

Back to fabrice's page