Publication Type:

Conference Paper

Source:

ACWR 2011 - Proceedings of the International Conference on Wireless Technologies for Humanitarian Relief, Amritapuri, p.165-168 (2011)

URL:

http://www.scopus.com/inward/record.url?eid=2-s2.0-84860792410&partnerID=40&md5=6d3560f75fae72dd1e31f34c28dbc000

Keywords:

Access points, Biomolecular system, Calculations, Concurrent process, Cross-layer, Emergency communication, Formal languages, Formal Specification, Formal specification and verification, Gateways (computer networks), Handoff algorithms, Level of abstraction, Mobile nodes, Mobile systems, Protocol agent, Protocol specifications, Rigorous analysis, Road safety, Security protocols, Specifications, Vehicular networks, Wireless telecommunication systems

Abstract:

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.

Notes:

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

Cite this Research Publication

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.