Foundations of ad hoc wireless networks
Citation:
Andrea Cerone, 'Foundations of ad hoc wireless networks', [thesis], Trinity College (Dublin, Ireland). School of Computer Science & Statistics, 2012, pp 246Download Item:
Abstract:
In this thesis we implement different process calculi to model ad hoc wireless networks. Each of these calculi considers different features of wireless systems, which are selected by focusing on the kind of applications or protocols that need to be analysed. In particular, we decided to take into account the following features: local broadcast a wireless network is represented as a collection of agents, called nodes (or stations); each node has the capability to broadcast messages and to wait for messages to be received. A graph is used to describe the topology of the network; a message broadcast by a node can be detected by all, and only all, its neighbours. All the neighbours because I wish to model ad hoc wireless networks, which employ broadcast communication. Only all, because every node has a range of transmission; the neighbours of a node, in the graph representing the network topology, are intuitively exactly those nodes which lie in its range of transmission, and have therefore the chance to receive the message. In this scenario, I make the assumption that communication is perfect; every time a message is broadcast by a node, all the nodes in its range of transmission can detect it correctly. As I shall note later, this amounts to assume that perfect communication is achieved by means of some protocol at the MAC sub-layer of the ISO/OSI reference model [69]. probabilistic behaviour the calculus described above is extended so that nodes exhibit random behaviour. There are several motivations for this extension. First, in the last decades there has been a growing research interest in the use of probabilistic protocols in wireless networks, which have been applied in different situations; see for example [14] or [59]. Second, ad hoc wireless networks are multi-agent systems. For such systems, there exist problems of high relevance that cannot be solved by deterministic protocols, but for which unbounded time probabilistic protocols have been exhibited and proved correct. One of the most famous problems in this family is distributed consensus [6] Time and collisions the calculi discussed above are suitable for the analysis of high level networks, specifically for the description of protocols and applications which lie at the internet layer, or at a higher one, in the ISO/OSI reference model. However, since the birth of wireless systems, protocols at lower layers, such as the MAC sub-layer, have been defined and analysed in detail; see [40] for a survey. To accomodate the needs of the research community, I decided to develop a process calculus in which the requirement that communication is perfect is dropped. In this calculus, broadcast of messages is modeled as a timed activity; they have a start phase and a end phase, during which time can pass. This constraint allows the modelling of situations in which a broadcast is performed while another one is in progress, causing a collision; that is, in this scenario a receiver detects a corrupted (noisy) message. I stress here that in this calculus the communication topology is flat; a broadcast can be detected by every station in the network. This is because the literature about collisions in wireless networks is relatively poor; in our own opinion, it is best to analyse an easier framework in order to understand in depth the semantics of broadcast processes subject to collision, rather than trying to accomplish the same task over frameworks which are more complicated both to define and analyse. For each of these calculi, the problem of defining a behavioural compositional theory is tackled. Compositional reasoning is very useful; in few words, it allows the analysis of the behaviour of complex (i.e. very iii iv large) networks by looking at the behaviour of two simpler networks, selected in a way that their composition coincides with the former one. However, it is important here to remark that the notion of composition of networks has to be stated precisely. In process calculi, such as CCS and CSP, composing two processes is a simple problem, as it is sufficient to define a set of structural operational semantics rules that state how two processes P and Q interact in their parallel composition P | Q. When dealing with networks the situation becomes more complicated. This is because networks are equipped with a topological structure by definition; processes are associated to nodes (or locations), and a notion of neighborhood between nodes is provided by a digraph. When composing two networks, we want at the same time to ensure that the topological structure of them is both preserved and non-corrupted. Preservation of the topological structure corresponds to requiring that two neighbouring nodes in a network are still neighbours when the latter is composed with another network; also, the process associated with a location has to be preserved. Non-corruption (or integrity) corresponds to requiring that no additional neighbours are introduced for any node in a network when it is composed with another one. In order to ensure these two properties, network composition has to be defined as a partial operator. For example, it is not possible to compose two networks which have different processes associated with the same location, as code preservation would not be ensured. While it is possible to define an operator that ensures preservation and integrity of networks, this approach has a severe limitation. Behavioural compositional preorders induced by this operator (such as the testing preorders [17]) turn out to be degenerate. That is, networks cannot be distinguished from each other. An alternative approach is that of weakening the constraints required by composition operator; given two networks M and N, we allow the structure of the latter to be corrupted in their composition M k> N. The main drawback of this weakening is that the composition operator is not symmetric anymore, so that compositional reasoning becomes more complex; however, the behavioural preorders it induces do not lead to a degenerate theory, and relating networks with different topological structure is possible. The study of behavioural preorders for networks constitutes the main contribution of this thesis. Testing behavioural preorders in the style of Hennessy and de Nicola are defined and analysed for each of the calculi above, and proof techniques for them are exhibited. This allows to demonstrate whether two networks cannot be distinguished by any test. Also, it is possible to check if a network satisfies a specification. This is done by exhibiting a simple network, for which it is straightforward to prove that it satisfies a desired (extensional) property; then, for any other network, it is sufficient to show that it is equivalent to the former one in order to ensure that it also satisfies the required property. We provide a wide range of applications that show how the proof techniques can be used to analyse practical situations and problems of interest. In this case, we decided to follow two different strands: Wireless Networks problems which are particular to (wireless) systems are taken into account; specifically we take into account the analysis of as routing protocols and connection protocols. Distributed Systems in this case both theoretical and practical problems in distributed systems are analysed; examples include the implementation of a virtual shared memory and the problem of consensus
Author: Cerone, Andrea
Advisor:
Hennessy, MatthewPublisher:
Trinity College (Dublin, Ireland). School of Computer Science & StatisticsNote:
TARA (Trinity's Access to Research Archive) has a robust takedown policy. Please contact us if you have any concerns: rssadmin@tcd.ieType of material:
thesisAvailability:
Full text availableMetadata
Show full item recordLicences: