Matching Items (60)

135810-Thumbnail Image.png

Testbed Implementation of the Meta-MAC Protocol

Description

The meta-MAC protocol is a systematic and automatic method to dynamically combine any set of existing Medium Access Control (MAC) protocols into a single higher level MAC protocol. The meta-MAC

The meta-MAC protocol is a systematic and automatic method to dynamically combine any set of existing Medium Access Control (MAC) protocols into a single higher level MAC protocol. The meta-MAC concept was proposed more than a decade ago, but until now has not been implemented in a testbed environment due to a lack of suitable hardware. This thesis presents a proof-of-concept implementation of the meta-MAC protocol by utilizing a programmable radio platform, the Wireless MAC Processor (WMP), in combination with a host-level software module. The implementation of this host module, and the requirements and challenges faced therein, is the primary subject of this thesis. This implementation can combine, with certain constraints, a set of protocols each represented as an extended finite state machine for easy programmability. To illustrate the combination principle, protocols of the same type but with varying parameters are combined in a testbed environment, in what is termed parameter optimization. Specifically, a set of TDMA protocols with differing slot assignments are experimentally combined. This experiment demonstrates that the meta-MAC implementation rapidly converges to non-conflicting TDMA slot assignments for the nodes, with similar results to those in simulation. This both validates that the presented implementation properly implements the meta-MAC protocol, and verifies that the meta-MAC protocol can be as effective on real wireless hardware as it is in simulation.

Contributors

Created

Date Created
  • 2016-05

136275-Thumbnail Image.png

On the Semantic Equivalence of a Program and Any of its Intermediate Representations

Description

The central goal of this thesis is to develop a practical approach to validating the correctness of SSA forms. Since achieving this goal is very involved for a general program,

The central goal of this thesis is to develop a practical approach to validating the correctness of SSA forms. Since achieving this goal is very involved for a general program, we restrict our attention to simple programs. In particular, the programs we consider are loop-free and are comprised of simple assignments to scalar variables, as well as input and output statements. Even for such a simple program, a full formal treatment would be very involved, extending beyond the scope of an undergraduate honors thesis.

Contributors

Created

Date Created
  • 2015-05

132967-Thumbnail Image.png

Learning Generalized Heuristics Using Deep Neural Networks

Description

Classical planning is a field of Artificial Intelligence concerned with allowing autonomous agents to make reasonable decisions in complex environments. This work investigates
the application of deep learning and planning

Classical planning is a field of Artificial Intelligence concerned with allowing autonomous agents to make reasonable decisions in complex environments. This work investigates
the application of deep learning and planning techniques, with the aim of constructing generalized plans capable of solving multiple problem instances. We construct a Deep Neural Network that, given an abstract problem state, predicts both (i) the best action to be taken from that state and (ii) the generalized “role” of the object being manipulated. The neural network was tested on two classical planning domains: the blocks world domain and the logistic domain. Results indicate that neural networks are capable of making such
predictions with high accuracy, indicating a promising new framework for approaching generalized planning problems.

Contributors

Created

Date Created
  • 2019-05

133211-Thumbnail Image.png

Beyond Deep Learning: Synthesizing Navigation Programs using Neural Turing Machines

Description

This thesis aims to improve neural control policies for self-driving cars. State-of-the-art navigation software for self-driving cars is based on deep neural networks, where the network is trained on a

This thesis aims to improve neural control policies for self-driving cars. State-of-the-art navigation software for self-driving cars is based on deep neural networks, where the network is trained on a dataset of past driving experience in various situations. With previous methods, the car can only make decisions based on short-term memory. To address this problem, we proposed that using a Neural Turing Machine (NTM) framework adds long-term memory to the system. We evaluated this approach by using it to master a palindrome task. The network was able to infer how to create a palindrome with 100% accuracy. Since the NTM structure proves useful, we aim to use it in the given scenarios to improve the navigation safety and accuracy of a simulated autonomous car.

Contributors

Agent

Created

Date Created
  • 2018-05

148109-Thumbnail Image.png

DSL for Spatio-Temporal Perception Logic Specifications

Description

System and software verification is a vital component in the development and reliability of cyber-physical systems - especially in critical domains where the margin of error is minimal. In the

System and software verification is a vital component in the development and reliability of cyber-physical systems - especially in critical domains where the margin of error is minimal. In the case of autonomous driving systems (ADS), the vision perception subsystem is a necessity to ensure correct maneuvering of the environment and identification of objects. The challenge posed in perception systems involves verifying the accuracy and rigidity of detections. The use of Spatio-Temporal Perception Logic (STPL) enables the user to express requirements for the perception system to verify, validate, and ensure its behavior; however, a drawback to STPL involves its accessibility. It is limited to individuals with an expert or higher-level knowledge of temporal and spatial logics, and the formal-written requirements become quite verbose with more restrictions imposed. In this thesis, I propose a domain-specific language (DSL) catered to Spatio-Temporal Perception Logic to enable non-expert users the ability to capture requirements for perception subsystems while reducing the necessity to have an experienced background in said logic. The domain-specific language for the Spatio-Temporal Perception Logic is built upon the formal language with two abstractions. The main abstraction captures simple programming statements that are translated to a lower-level STPL expression accepted by the testing monitor. The STPL DSL provides a seamless interface to writing formal expressions while maintaining the power and expressiveness of STPL. These translated equivalent expressions are capable of directing a standard for perception systems to ensure the safety and reduce the risks involved in ill-formed detections.

Contributors

Agent

Created

Date Created
  • 2021-05

151851-Thumbnail Image.png

Dynamic programming algorithm for computing temporal logic robustness

Description

In this thesis we deal with the problem of temporal logic robustness estimation. We present a dynamic programming algorithm for the robust estimation problem of Metric Temporal Logic (MTL) formulas

In this thesis we deal with the problem of temporal logic robustness estimation. We present a dynamic programming algorithm for the robust estimation problem of Metric Temporal Logic (MTL) formulas regarding a finite trace of time stated sequence. This algorithm not only tests if the MTL specification is satisfied by the given input which is a finite system trajectory, but also quantifies to what extend does the sequence satisfies or violates the MTL specification. The implementation of the algorithm is the DP-TALIRO toolbox for MATLAB. Currently it is used as the temporal logic robust computing engine of S-TALIRO which is a tool for MATLAB searching for trajectories of minimal robustness in Simulink/ Stateflow. DP-TALIRO is expected to have near linear running time and constant memory requirement depending on the structure of the MTL formula. DP-TALIRO toolbox also integrates new features not supported in its ancestor FW-TALIRO such as parameter replacement, most related iteration and most related predicate. A derivative of DP-TALIRO which is DP-T-TALIRO is also addressed in this thesis which applies dynamic programming algorithm for time robustness computation. We test the running time of DP-TALIRO and compare it with FW-TALIRO. Finally, we present an application where DP-TALIRO is used as the robustness computation core of S-TALIRO for a parameter estimation problem.

Contributors

Agent

Created

Date Created
  • 2013

152324-Thumbnail Image.png

Incorporating supervisory human inputs into autonomous robot navigation

Description

With robots being used extensively in various areas, a certain degree of robot autonomy has always been found desirable. In applications like planetary exploration, autonomous path planning and navigation are

With robots being used extensively in various areas, a certain degree of robot autonomy has always been found desirable. In applications like planetary exploration, autonomous path planning and navigation are considered essential. But every now and then, a need to modify the robot's operation arises, a need for a human to provide it some supervisory parameters that modify the degree of autonomy or allocate extra tasks to the robot. In this regard, this thesis presents an approach to include a provision to accept and incorporate such human inputs and modify the navigation functions of the robot accordingly. Concepts such as applying kinematical constraints while planning paths, traversing of unknown areas with an intent of maximizing field of view, performing complex tasks on command etc. have been examined and implemented. The approaches have been tested in Robot Operating System (ROS), using robots such as the iRobot Create, Personal Robotics (PR2) etc. Simulations and experimental demonstrations have proved that this approach is feasible for solving some of the existing problems and that it certainly can pave way to further research for enhancing functionality.

Contributors

Agent

Created

Date Created
  • 2013

152179-Thumbnail Image.png

Model-based design, simulation and automatic code generation for embedded systems and robotic applications

Description

As the complexity of robotic systems and applications grows rapidly, development of high-performance, easy to use, and fully integrated development environments for those systems is inevitable. Model-Based Design (MBD) of

As the complexity of robotic systems and applications grows rapidly, development of high-performance, easy to use, and fully integrated development environments for those systems is inevitable. Model-Based Design (MBD) of dynamic systems using engineering software such as Simulink® from MathWorks®, SciCos from Metalau team and SystemModeler® from Wolfram® is quite popular nowadays. They provide tools for modeling, simulation, verification and in some cases automatic code generation for desktop applications, embedded systems and robots. For real-world implementation of models on the actual hardware, those models should be converted into compilable machine code either manually or automatically. Due to the complexity of robotic systems, manual code translation from model to code is not a feasible optimal solution so we need to move towards automated code generation for such systems. MathWorks® offers code generation facilities called Coder® products for this purpose. However in order to fully exploit the power of model-based design and code generation tools for robotic applications, we need to enhance those software systems by adding and modifying toolboxes, files and other artifacts as well as developing guidelines and procedures. In this thesis, an effort has been made to propose a guideline as well as a Simulink® library, StateFlow® interface API and a C/C++ interface API to complete this toolchain for NAO humanoid robots. Thus the model of the hierarchical control architecture can be easily and properly converted to code and built for implementation.

Contributors

Agent

Created

Date Created
  • 2013

151405-Thumbnail Image.png

Model based safety analysis and verification of cyber-physical systems

Description

Critical infrastructures in healthcare, power systems, and web services, incorporate cyber-physical systems (CPSes), where the software controlled computing systems interact with the physical environment through actuation and monitoring. Ensuring software

Critical infrastructures in healthcare, power systems, and web services, incorporate cyber-physical systems (CPSes), where the software controlled computing systems interact with the physical environment through actuation and monitoring. Ensuring software safety in CPSes, to avoid hazards to property and human life as a result of un-controlled interactions, is essential and challenging. The principal hurdle in this regard is the characterization of the context driven interactions between software and the physical environment (cyber-physical interactions), which introduce multi-dimensional dynamics in space and time, complex non-linearities, and non-trivial aggregation of interaction in case of networked operations. Traditionally, CPS software is tested for safety either through experimental trials, which can be expensive, incomprehensive, and hazardous, or through static analysis of code, which ignore the cyber-physical interactions. This thesis considers model based engineering, a paradigm widely used in different disciplines of engineering, for safety verification of CPS software and contributes to three fundamental phases: a) modeling, building abstractions or models that characterize cyberphysical interactions in a mathematical framework, b) analysis, reasoning about safety based on properties of the model, and c) synthesis, implementing models on standard testbeds for performing preliminary experimental trials. In this regard, CPS modeling techniques are proposed that can accurately capture the context driven spatio-temporal aggregate cyber-physical interactions. Different levels of abstractions are considered, which result in high level architectural models, or more detailed formal behavioral models of CPSes. The outcomes include, a well defined architectural specification framework called CPS-DAS and a novel spatio-temporal formal model called Spatio-Temporal Hybrid Automata (STHA) for CPSes. Model analysis techniques are proposed for the CPS models, which can simulate the effects of dynamic context changes on non-linear spatio-temporal cyberphysical interactions, and characterize aggregate effects. The outcomes include tractable algorithms for simulation analysis and for theoretically proving safety properties of CPS software. Lastly a software synthesis technique is proposed that can automatically convert high level architectural models of CPSes in the healthcare domain into implementations in high level programming languages. The outcome is a tool called Health-Dev that can synthesize software implementations of CPS models in healthcare for experimental verification of safety properties.

Contributors

Agent

Created

Date Created
  • 2012

151431-Thumbnail Image.png

Replay debugger for human interactive multiple threaded android applications

Description

Debugging is a boring, tedious, time consuming but inevitable step of software development and debugging multiple threaded applications with user interactions is even more complicated. Since concurrency and synchronism are

Debugging is a boring, tedious, time consuming but inevitable step of software development and debugging multiple threaded applications with user interactions is even more complicated. Since concurrency and synchronism are normal features in Android mobile applications, the order of thread execution may vary in every run even with the same input. To make things worse, the target erroneous cases may happen just in a few specific runs. Besides, the randomness of user interactions makes the whole debugging procedure more unpredictable. Thus, debugging a multiple threaded application is a tough and challenging task. This thesis introduces a replay mechanism for debugging user interactive multiple threaded Android applications. The approach is based on the 'Lamport Clock' concept, 'Event Driven' implementation and 'Client-Server' architecture. The debugger tool described in this thesis provides a user controlled debugging environment where users or developers are allowed to use modified record application to generate a log file. During the record time, all the necessary events like thread creation, synchronization and user input are recorded. Therefore, based on the information contained in the generated log files, the debugger tool can replay the application off-line since log files provide the deterministic order of execution. In this case, user or developers can replay an application as many times as they need to pinpoint the errors in the applications.

Contributors

Agent

Created

Date Created
  • 2012