January 9, 2013
Andrea Cerone
We present a process calculus for modelling wireless networks at the Network Layer of the ISO/OSI reference model, that is where point-to-point reliable broadcast is the only communication mechanism between stations. We introduce a theory of composition of networks, which is used as a basis for developing behavioural preorders in the style of Hennessy and de Nicola. We also provide sound and complete proof techniques for showing whether two networks are related according to one of such preorders. Finally, we show the usefulness of our proof techniques by verifying the correct behaviour of a routing protocol with respect to a formal specification.