From ABC of Networks to a LitTLe logic for mobilityPublished: Tuesday, 29 May 2018
School Seminar on Wednesday 30th May 2018 at 2pm in Kilburn L.T 1.4 Title: From ABC of Networks to a LitTLe logic for mobility by Sanjiva Prasad (IIT Delhi) Abstract:We examine the essential invariants that guarantee correct delivery of ...
School Seminar on Wednesday 30th May 2018 at 2pm in Kilburn L.T 1.4
Title: From ABC of Networks to a LitTLe logic for mobility by Sanjiva Prasad (IIT Delhi)
Abstract:We examine the essential invariants that guarantee correct delivery of messages in network protocols supporting mobility. In the past 20 years, the Mobile IP model has posed a challenge to formal verification, though several attempts using process calculi and model checking have been attempted with varying degrees of success, often positing stronger requirements than are strictly necessary.
In this talk we revisit the problem, starting from the model of Abstract Switches presented in the axiomatic basis for communication (ABC) proposed by Karsten et al which we reformulated using LTL to examine networks whose routing/forwarding behaviour can vary over time. This allowed a new proof of correctness of the core property of the IPv6 protocol, i.e, that if a mobile node remains stationed at a host ``long enough’’, data messages addressed to it will eventually get delivered.
We then show how this correctness of IPv6 (a liveness property) can be established by model-checking a bounded liveness property on a small model, and using parametric verification techniques. This approach works for the IP mobility model since the system eventually converges to a ``stable’' subsystem on which established abstraction and model checking techniques are effective.
Short Bio: Sanjiva Prasad is a Professor at the Indian Institute of Technology Delhi, where he has worked from 1994. He completed his B.Tech from IIT Kanpur in 1985, and his PhD from Stony Brook University, NY in 1991, and has worked in research centres and universities in the US, Germany and Denmark. His main research interests are in programming language semantics, process calculi, mobile computing, Formal Methods and verification. He is currently also involved in research in the use of IT for medical applications, and security in IoT.
Refreshments and informal discussions will be held in the Staff Common room after the seminar