Model Checking MANETs with Arbitrary Mobility
Modeling arbitrary connectivity changes of mobile ad hoc networks (MANETs) makes application of automated formal verification challenging. We introduced constrained labeled transition systems (CLTSs) as a semantic model to represent mobility. To model che
- PDF / 806,505 Bytes
- 16 Pages / 439.37 x 666.142 pts Page_size
- 49 Downloads / 191 Views
2
University of Tehran, Tehran, Iran VU University Amsterdam, Amsterdam, The Netherlands 3 Sharif University of Technology, Tehran, Iran
Abstract. Modeling arbitrary connectivity changes of mobile ad hoc networks (MANETs) makes application of automated formal verification challenging. We introduced constrained labeled transition systems (CLTSs) as a semantic model to represent mobility. To model check MANET protocol with respect to the underlying topology and connectivity changes, we here introduce a branching-time temporal logic interpreted over CLTSs. The temporal operators, from Action Computation Tree Logic with an unless operator, are parameterized by multi-hop constraints over topologies, to express conditions on successful scenarios of a MANET protocol. We moreover provide a bisimilarity relation with the same distinguishing power for CLTSs as our logical framework.
1
Introduction
In mobile ad hoc networks (MANETs), nodes communicate along multi-hop paths using wireless transceivers. Wireless communication is restricted; only nodes located in the range of a transmitter receive data. Due to e.g. noise in the environment, interferences, and temporary communication link errors, wireless communication is unreliable, which together with mobility of nodes complicates the design of MANET protocols. Formal methods provide valuable tools to design, evaluate and verify such protocols. We introduced Restricted Broadcast Process Theory (RBPT) [9] to specify and verify MANETs, taking into account mobility. RBPT specifies a MANET by composing nodes using a restricted local broadcast operator. A strong point of RBPT is that the underlying topology is not specified in the syntax, which would make it hard to set up the initial topology for each scenario in a verification. In similar approaches, the mobility is modeled as arbitrary manipulation of the underlying topology (given as part of the semantic state), which may make the model infinite and insusceptible to automated verification techniques. Instead in the semantic model of RBPT, a constraint labeled transition system (CLTS) [10], transitions are enriched with so-called network constraints, to restrict the possible topologies. This symbolic representation of network topologies in the semantics is more compact and allows automated verification techniques to investigate families of properties on a unified model. F. Arbab and M. Sirjani (Eds.): FSEN 2013, LNCS 8161, pp. 217–232, 2013. DOI: 10.1007/978-3-642-40213-5 14, c IFIP International Federation for Information Processing 2013
218
F. Ghassemi et al.
Properties in MANETs tend to be weaker than in wired networks, due to the topology-dependent behavior of communication, and consequently the need for multi-hop communication between nodes. For instance, an important property in routing or information dissemination protocols is packet delivery: If there exists an end-to-end route between two nodes A and B for a long enough period of time, then packets sent by A will be received by B [7]. To reason about properties that r
Data Loading...
