Skip to Main content Skip to Navigation
Poster communications

TORA, Verification, Proofs and Model Checking

Abstract : Routing protocols for mobile adhoc networks (MANET) are one of the most essential components of such networks; the other being media access control (MAC) protocols. Unfortunately most existing routing protocols for MANETs are so complex that the investigation of their properties, weaknesses and performance cannot be done analytically (at least using conventional analytic methods); instead simulations have become the typical means of analyzing their properties and performance. This is an unfortunate state of affairs for such an important networking component. In this paper we develop a different means for analyzing the properties and performance of routing protocols for MANETs based on methods and techniques from formal specifications [3] and associated formal means for proof and validation. The aim is to develop rigorous proofs and tools for performance checking and analysis. The primary goal of this type of research is to develop a way to automatically check a specification for correctness and liveness properties. A secondary, but equally important role is the development of automatic tools for ameliorating discovered weaknesses and for designing such routing protocols so as to satisfy prespecified properties and performance.
Complete list of metadata
Contributor : Service Ist Inria Sophia Antipolis-Méditerranée / I3s Connect in order to contact the contributor
Submitted on : Monday, March 22, 2010 - 1:59:51 PM
Last modification on : Monday, March 22, 2010 - 2:57:42 PM
Long-term archiving on: : Friday, June 25, 2010 - 11:46:20 AM


Files produced by the author(s)


  • HAL Id : inria-00465989, version 1



Shah-An yang, John S. Baras. TORA, Verification, Proofs and Model Checking. WiOpt'03: Modeling and Optimization in Mobile, Ad Hoc and Wireless Networks, Mar 2003, Sophia Antipolis, France. 2 p. ⟨inria-00465989⟩



Record views


Files downloads