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.

This thesis presents the design, development, and testing of a multi-agent systems laboratory that will enable the experimental investigation of Networked Control Systems. Networked Control Systems (NCS) are integrations of computation, networking, and physical dynamics, in which embedded devices are networked to sense, monitor, execute collaborative tasks, and interact with the physical world. As the potential for applications of NCS has increased, so has the research interest in this area. Possible applications include search and rescue, scientific data collection, and health care monitoring systems. One of the primary challenges in applying NCS is designing distributed algorithms that will enable the networked devices to achieve global objectives. Another challenge is in ensuring that distributed algorithms have the necessary robustness to achieve those global objectives in dynamic and unpredictable environments. A multi-agent systems laboratory provides the researcher with a means to observe the behavior and performance of distributed algorithms as they are executed on a set of networked devices. Through this observation, the researcher may discover robustness issues that were not present in computer simulation. The objective of this research is to design and implement the infrastructure for a multi-agent systems laboratory to observe distributed algorithms implemented on networked devices.

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.