No description available.

Thesis (M.Sc.)--York University, 2007. Graduate Programme in Computer Science and Engineering. / Typescript. Includes bibliographical references (leaves 170-173). Also available on the Internet. MODE OF ACCESS via web browser by entering the following URL: http://gateway.proquest.com/openurl?url_ver=Z39.88-2004&res_dat=xri:pqdiss&rft_val_fmt=info:ofi/fmt:kev:mtx:dissertation&rft_dat=xri:pqdiss:MR38826

Doctor of Philosophy / Department of Computing and Information Sciences / Gurdip Singh / To increase their applicability, distributed algorithms are typically written to work with any application on any network. This flexibility comes at the cost of performance since these 'general purpose' algorithms are written with the worst case scenario in mind. A distributed algorithm written for a specific application or a class of application is fine tuned to the properties of the application and can give a better performance when compared to the general purpose one. In this work, we propose two mechanisms in which we can optimize a general purpose algorithm - Alg based on the application - App using it. In the first approach, we analyze the specification of App to identify patterns of communication in its communication topology. These properties are then used to customize the behavior of the underlying distributed algorithm Alg. To demonstrate this approach, we study applications specified as component based systems where application components communicate via events and distributed algorithms to enforce ordering requirements on these events. We show how our approach can be used to optimize event ordering algorithms based on communication patterns in the applications. In the second approach, rather than analyzing the application specification, we assume that the developer provides application properties - I_App which are invariants for the optimization process. We assume that the algorithm is written and annotated in a format that is amenable to analysis. Our analysis algorithm then takes as input the application invariants and the annotated algorithm and looks for potential functions in the algorithm which are redundant in the context of the given application. In particular, we first look for function invocations in the algorithm whose post-conditions are already satisfied as a result of the application invariants. Each such invocation is considered as a potential redundant module. We further analyze the distributed algorithm to identify the impact of the removal of a specific invocation on the rest of the algorithm. We describe an implementation of this approach and demonstrate the applicability using a distributed termination detection algorithm.

Master of Science / Department of Computing and Information Sciences / Gurdip Singh / PROMELA stands for Protocol Meta Language. It is a modeling language for developing distributed systems. It allows for the dynamic creation of concurrent processes which can communicate through message channels. DAJ stands for Distributed Algorithms in Java. It is a Java toolkit for designing, implementing, simulating, and visualizing distributed algorithms. The toolkit consists of Java class library with a simple programming interface that allows development of distributed algorithms based on a message passing model. It also provides a visualization environment where the protocol execution can be paused, performed step by step, and restarted. This project is a Java application designed to translate a model written in Promela into a model using the Java class library provided by DAJ and simulate it using DAJ. Even though there are similarities between the programming constructs of Promela and DAJ, the programming interface supported by DAJ is smaller, so the input has been confined to a variant, which is a subset of Promela. The implementation was performed in three steps. In the first step an input domain was defined and an ANTLR grammar was defined for the input structure. Java code has been embedded to this ANTLR grammar so that it can parse the input and translates it into an intermediate xml format. In the second step, a String Template is used which would consist of templates of the output model, along with a Java program which traverses the intermediate xml file and generates the output model. In the third step, the obtained output model is compiled and then simulated and visualized using DAJ. The application has been tested over input models having different topologies, process nodes, messages, and variables and covering most of the input domain.

This thesis was motivated by a case study involving the formalisation of arguments that simplify the verification of tree-oriented multicast protocols. As well as covering the case study itself, it discusses our solution to problems we encountered concerning expressivity and automation. The expressivity problems related to the need for theory interpretation. We found the existing Locale and axiomatic type class mechanisms provided by the Isabelle theorem prover we were using to be inadequate. This led us to develop a new prototype implementation of theory interpretation. To support this implementation, we developed a novel system of proof terms for the HOL logic that we also describe in this thesis. We found existing automation to perform poorly, which led us to experiment with additional kinds of automation. We describe our approach, focusing on features that make automation suitable for interactive use. Our presentation of the case study starts with our formalisation of an abstract theory of distributed systems, covering state transition systems, forward and backward simulation relations, and related properties of LTL (linear temporal logic). We then summarise proofs of simulation relations holding for particular abstract multicast protocols. We discuss the mechanisation styles we experimented with in the case study. We also discuss the methodology behind our proofs. We cover aspects such as how to discover and construct proofs, and how to explore the space of proofs, how to make good definitions and lemmas, how to increase modularity, reuse, stability and malleability of proofs, and reduce maintenance of proofs, and the gap between intuitively understood proofs and their formalisation.

No description available.

Ο σκοπός αυτής της διατριβής είναι να αναπτυχθούν σχέδια συντονισμού σχετικά με την κίνηση των ρομποτικών πρακτόρων με σκοπό την κάλυψη μιας περιοχής κάτω από RF επικοινωνιακούς περιορισμούς . Οι κόμβοι εκτελούν την κίνηση σε ξεχωριστά χρονικά βήματα σύμφωνα με τις διανεμημένες πληροφορίες που αποκτώνται από τους κόμβους που συνδέονται στον προκαθορισμένο αριθμό hops έως ότου φθάσουν στη βέλτιστη τοπολογία όσον αφορά την κάλυψη της περιοχής. Τα ρομπότ υποτίθεται ότι είναι εξοπλισμένα με έναν αισθητήρα για λόγους κάλυψης και με έναν ράδιο πομποδέκτη έτσι ώστε να μεταδοθούν οι πληροφορίες. Ωστόσο, η ακτίνα επικοινωνίας δεν απαιτείται να είναι τουλάχιστον διπλάσια της ακτίνας του αισθητήρα επισκόπησης, κάτι που προσθέτει έναν πρόσθετο περιορισμό στο γενικό πρόβλημα. Τα σχέδια συντονισμού αναπτύσσονται εξασφαλίζοντας την συνολική RF συνδεσιμότητα του δικτύου επιτυγχάνοντας τη βέλτιστη κάλυψη περιοχής. Τα αποτελέσματα ελέγχονται περαιτέρω μέσω των μελετών προσομοιώσεων. / The purpose of this thesis is to develop coordination schemes concerning the motion of robotic agents for area coverage purposes under RF communications constraints. The nodes perform motion in discrete time steps according to distributed information acquired from nodes which are connected at predefined number of hops until they reach optimum area configuration. Robots are supposed to be equipped with sensor for coverage purposes and with radio transceiver so as information to be transmitted. However, communication radius is not demanded to be at least equal to twice the sensing one, imposing an extra constraint in the overall problem. Coordination schemes are developed ensuring end-to-end RF connectivity of the network while attaining optimum area coverage. Results are further verified via simulations studies.

No description available.

Doctor of Philosophy / Department of Computing and Information Sciences / Gurdip Singh / Many frameworks have been proposed which provide distributed algorithms encapsulated as middleware services to simplify application design. The developers of such algorithms are faced with two opposing forces. One is to design generic algorithms that are reusable in a large number of applications. Efficiency considerations, on the other hand, force the algorithms to be customized to specific operational contexts. This problem is often attacked by simply re-implementing all or large portions of an algorithm. We propose InDiGO, an infrastructure which allows design of generic but customizable algorithms and provides tools to customize such algorithms for specific applications. InDiGO provides the following capabilities: (a) Tools to generate intermediate representations of an application which can be leveraged for analysis, (b) Mechanisms to allow developers to design customizable algorithms by exposing design knowledge in terms of configurable options, and (c) An optimization engine to analyze an application to derive the information necessary to optimize the algorithms. Specifically, we optimize algorithms by removing communication which is redundant in the context of a specific application. We perform three types of optimizations: static optimization, dynamic optimization and physical topology-based optimization. We present experimental results to demonstrate the advantages of our infrastructure.

Hui, Tan Hing. / Thesis (M.Phil.)--Chinese University of Hong Kong, 2011. / Includes bibliographical references (p. 151-162). / Abstracts in English and Chinese. / Abstract --- p.i / Acknowledgement --- p.vi / Chapter 1 --- Introduction --- p.1 / Chapter 2 --- Literature Review --- p.7 / Chapter 2.1 --- Background --- p.7 / Chapter 2.1.1 --- "Tools for Analyzing Vehicles' Speeds, Traffic Flows and Densities" --- p.7 / Chapter 2.1.2 --- Tools for Analyzing Bytes Received by the Vehicles from an AP --- p.9 / Chapter 2.1.3 --- Effort-Fairness vs Outcome-Fairness --- p.10 / Chapter 2.1.4 --- Quantifying Fairness on the Bytes Received by the Vehicles from an AP --- p.10 / Chapter 2.2 --- Delay-Tolerant Networks(DTNs) --- p.12 / Chapter 2.3 --- Drive-thru Internet Systems --- p.14 / Chapter 2.4 --- Resource Allocation/Scheduling in Drive-thru Internet and Related Systems --- p.20 / Chapter 2.4.1 --- Resource Allocation/Scheduling Algorithms for Multiple Vehicles --- p.20 / Chapter 2.4.2 --- Rate Adaptation Algorithms for Fast-varying Channels due to Vehicular Movement/Mobility --- p.29 / Chapter 3 --- Performance Evaluation of Round-robin Scheduler with IEEE 802.11 MAC --- p.33 / Chapter 3.1 --- System Model --- p.34 / Chapter 3.2 --- Description of the Real-life Vehicular Traffic Trace --- p.36 / Chapter 3.2.1 --- Analysis on Hourly Single-lane Traffic Flow of 1-80 Highway --- p.40 / Chapter 3.2.2 --- Analysis on Hourly Directional Traffic Flow of 1-80 Highway --- p.43 / Chapter 3.2.3 --- Analysis on Hourly Single-lane Vehicles' Speeds of 1-80 Highway --- p.45 / Chapter 3.2.4 --- Analysis on Daily Vehicles' Speeds of 1-80 Highway --- p.48 / Chapter 3.2.5 --- "Relationship among Average Traffic Densities, Flows and Vehicles' Speeds in Singlelane Scenarios" --- p.51 / Chapter 3.2.6 --- "Relationship among Average Traffic Densities, Flows and Vehicles' Speeds in Multilane Scenarios" --- p.52 / Chapter 3.3 --- Trace-driven Simulations of Drive-thru Internet Scenarios using Round-robin Scheduler with IEEE 802.11 MAC --- p.54 / Chapter 3.3.1 --- Simulation Setup --- p.54 / Chapter 3.3.2 --- Scenarios of using Fixed Data Rate --- p.57 / Chapter 3.3.3 --- Scenario of using Auto-rate Algorithm --- p.67 / Chapter 4 --- The Design and Implementation of VECADS --- p.73 / Chapter 4.1 --- Towards the Design of an Intelligent Scheduling for Drive-thru Internet --- p.74 / Chapter 4.1.1 --- System Throughput Maximization vs Fairness --- p.74 / Chapter 4.1.2 --- Antenna --- p.75 / Chapter 4.1.3 --- Speed --- p.76 / Chapter 4.1.4 --- Noisy Measurement of Predicting Channel Condition based on RSSI(or Similar Metrics) only --- p.77 / Chapter 4.1.5 --- Region for Serving “Weak´ح Vehicles --- p.78 / Chapter 4.2 --- System Model --- p.79 / Chapter 4.3 --- The Design of VECADS --- p.83 / Chapter 4.3.1 --- Using Vehicular Context to Help Scheduling --- p.83 / Chapter 4.3.2 --- Penalizing Slow Vehicles in the Coverage . --- p.88 / Chapter 4.3.3 --- "Round-Robin Scheduling for ""Weak"" Vehicles in the “Sweet Zone´ح" --- p.90 / Chapter 4.3.4 --- Rate Adaptation Algorithm in VEC ADS --- p.94 / Chapter 4.4 --- The Implementation of VECADS --- p.97 / Chapter 4.4.1 --- Overall System Architecture of VECADS --- p.97 / Chapter 4.4.2 --- Overall Scheduling Flow of VECADS --- p.100 / Chapter 4.4.3 --- Algorithms in VECADS --- p.102 / Chapter 5 --- Performance Evaluation of VECADS --- p.110 / Chapter 5.1 --- Simulation Setup --- p.110 / Chapter 5.2 --- Simulation Results and Discussion --- p.114 / Chapter 5.2.1 --- Evaluation of the Performance Impact of Different System Parameters --- p.114 / Chapter 5.2.2 --- Evaluation of Different Design Options --- p.119 / Chapter 6 --- Conclusions and Discussion --- p.142 / Chapter A --- Average Bytes Received by a Moving Vehicle from a Roadside AP --- p.146 / Chapter B --- Distribution of the Cumulative Bytes Received by Vehicles from a Roadside AP --- p.148 / Bibliography --- p.151