Objectives of the course

• Introduction to wireless protocols

• Challenges and problems in modelling and verifying such protocols

• Modelling techniques such as process algebra and (timed) automata

• Presentation of different verification approaches, including pen-and-paper, model checking and interactive theorem provers

• Comparison between these techniques

• Combining different approaches to achieve beoer verification techniques/tools

• Open research problems such as proper handling of dynamic topologies in model checking

All concepts will be illustrated by case studies of protocols used in real life, such as the AODV routing protocol.

The course begins with an introduction of protocol modelling and verification. It presents common techniques to model and verification techniques. Although these techniques are standard, it is not common that a course present industrial case studies. The second part of the course will cover current research and research challenges. It will illustrate the students the kind of challenges verification (of wireless protocols) faces. A particular focus will be given to modelling Ð an ability students need in industrial life. For this the lectures will be accompanied with a series of tutorial/lab hours, where students will model protocols on their own (under close supervision) and learn how to use model-checking tools.

Link to Osiris (University of Twente)

The course is also listed at Osiris, the student information system in use at the University of Twente. The course code is 201600266.