Bibliothèque de L'IMIST/CNRST

PH.D Université Mohammed V 2017

The continuous growth of complex systems across different areas in modern life makes the development of correct software increasingly important. However, software often contains errors. This increases the development costs, and makes software systems vulnerable. Guaranteeing reliability is therefore crucial, especially when the cost of failure is expensive in monetary terms and even more crucial when human safety is at risk. To deal with reliability and correctness, formal methods offer rigorous mathematical techniques to model and verify the systems. Event-B is one of these formal methods. Event-B is a recent formalism for specification and verification of software and hardware systems. It is supported by an extensible tool called Rodin. During recent years, Event-B and Rodin have been increasingly used in the development of systems across different critical and non-critical domains. In this thesis, after an in- depth study of Event-B, we have applied Event-B approach to protocol engineering activities such as protocol specification and verification.
Increasingly numerous and complex communication protocols are being employed in distributed systems and computer networks of various types. Therefore, it is vitally important to ensure that they work correctly and do not contain errors. The use of Event-B supports all relevant phases of protocol development and results in the creation of precise models that can be formally verified early during the development cycle.
In this research, our interest is focused on protocols with Voice over IP (VoIP), ARQ protocols and security protocols. Many protocols are chosen to be modeled and verified to describe how they work and prove their correctness. In our approach, a protocol specification written in a natural language is examined before modeling in order to plan the modeling and refinement strategy. After that, starting from a simple abstract model, concrete

models in several different abstraction levels are constructed by gradually introducing complex structures and concepts. Each refinement step is accompanied by proof obligations which must be discharged in order to verify its correctness.