Vehicular networking is an important emerging area having immense applications, ranging from road-safety to emergency communications in disaster situations. As more applications begin to take advantage of vehicular networks, correctness of the underlying protocols must be subjected to rigorous analysis. The π-calculus is a formal language for specifying mobile systems and has been applied in wide range of settings, from specifying security protocols to modeling biomolecular systems. In this paper, we use π-calculus to construct a formal specification of a cross-layer dual-radio handoff algorithm for vehicular networks. The main challenge in this work was to use the minimal set of highly expressive and powerful constructs of π-calculus to model protocol agents at the right level of abstraction. To give two instances of our approach: (a) the two radios involved in handoff are modelled as concurrent sub-processes of the mobile node process; (b) route to the gateway is modelled as a channel that the access point supplies to both the gateway and the mobile node, both of which are modelled as concurrent processes. We formulate representative properties in a branching-time temporal logic and verify our protocol specification against these properties. Our study shows that π-calculus is a suitable formalism for modeling and verifying vehicular protocols.
cited By (since 1996)0; Conference of org.apache.xalan.xsltc.dom.DOMAdapter@5290cba8 ; Conference Date: org.apache.xalan.xsltc.dom.DOMAdapter@202aacf1 Through org.apache.xalan.xsltc.dom.DOMAdapter@51c012b6; Conference Code:89682
Ja Poroor and Jayaraman, Bb, “Formal specification and verification of vehicular handoff using π-calculus”, in ACWR 2011 - Proceedings of the International Conference on Wireless Technologies for Humanitarian Relief, Amritapuri, 2011, pp. 165-168.