Open Access. Powered by Scholars. Published by Universities.®

Physical Sciences and Mathematics Commons

Open Access. Powered by Scholars. Published by Universities.®

Articles 1 - 13 of 13

Full-Text Articles in Physical Sciences and Mathematics

Mechanical And Modular Verification Condition Generation For Object-Based Software, Heather Harton Dec 2011

Mechanical And Modular Verification Condition Generation For Object-Based Software, Heather Harton

All Dissertations

The foundational goal of this work is the development of mechanizable proof rules and a verification condition generator based on those rules for modern software. The verification system will be modular so that it is possible to verify the implementation of a component relying upon only the specifications of underlying components that are reused. The system must enable full behavioral verification. The proof rules used to generate verification conditions (VCs) of correctness must be amenable to automation. While automation requires software developers to annotate implementations with assertions, it should not require assistance in the proofs. This research has led to …


A Web-Integrated Environment For Component-Based Software Reasoning, Charles Cook Dec 2011

A Web-Integrated Environment For Component-Based Software Reasoning, Charles Cook

All Theses

This thesis presents the Web IDE, a web-integrated environment for component-based software reasoning. The Web IDE is specifically tailored to emphasize the relationships among various components in component-based software engineering (CBSE) and to facilitate reasoning. It allows students to use RESOLVE, a component-based, integrated specification and programming language, to build components and systems, providing real-time feedback that can be used to reason about the correctness of their component implementations. Real-time interaction and relationship focused component presentation reinforces CBSE and reasoning principles in a way not possible with traditional programming exercises and file management systems.
The Web IDE has gone through …


Rigging And Texturing Considerations For The Short Film Spider Fight, Casey Johnson Dec 2011

Rigging And Texturing Considerations For The Short Film Spider Fight, Casey Johnson

All Theses

This paper delves into two separate production areas of the short film, Spider Fight: the approach used to solve the problem of rigging eyelids for 3d characters, and the pipelines that were implemented for texturing 3d assets. Typically, problems exist in the rigging of eyelids for 3d characters. Productions rely on a series of blend shapes, or a combination of joints and blend shapes, to produce satisfactory eyelid movement. Spider Fight, however, used a series of curves and joints to control the movement of the eyelids, which allowed a high degree of control over eyelid movement, and also fast editing …


Data-Intensive Computing For Bioinformatics Using Virtualization Technologies And Hpc Infrastructures, Pengfei Xuan Dec 2011

Data-Intensive Computing For Bioinformatics Using Virtualization Technologies And Hpc Infrastructures, Pengfei Xuan

All Theses

The bioinformatics applications often involve many computational components and massive data sets, which are very difficult to be deployed on a single computing machine. In this thesis, we designed a data-intensive computing platform for bioinformatics applications using virtualization technologies and high performance computing (HPC) infrastructures with the concept of multi-tier architecture, which can seamlessly integrate the web user interface (presentation tier), scientific workflow (logic tier) and computing infrastructure (data/computing tier). We demonstrated our platform on two bioinformatics projects. First, we redesigned and deployed the cotton marker database (CMD) (http://www.cottonmarker.org), a centralized web portal in the cotton research community, using the …


The Design & Implementation Of An Abstract Semantic Graph For Statement-Level Dynamic Analysis Of C++ Applications, Edward Duffy Dec 2011

The Design & Implementation Of An Abstract Semantic Graph For Statement-Level Dynamic Analysis Of C++ Applications, Edward Duffy

All Dissertations

In this thesis, we describe our system, Hylian, for statement-level analysis,
both static and dynamic, of a C++ application. We begin by extending the
GNU gcc parser to generate parse trees in XML format for each of the
compilation units in a C++ application. We then provide verification that the
generated parse trees are structurally equivalent to the code in the
original C++
application. We use the generated parse trees, together with an augmented
version of the gcc test suite, to recover a grammar for the C++ dialect that
we parse. We use the recovered grammar to generate a schema …


Integrating Pixologic Zbrush Into An Autodesk Maya Pipeline, Micah Guy Aug 2011

Integrating Pixologic Zbrush Into An Autodesk Maya Pipeline, Micah Guy

All Theses

The purpose of this thesis is to integrate the use of the relatively new volumetric pixel program, Pixologic ZBrush, into an Autodesk Maya project pipeline. As ZBrush is quickly becoming the industry standard in advanced character design in both film and video game work, the goal is to create a succinct and effective way for Maya users to utilize ZBrush files. Furthermore, this project aims to produce a final film of both valid artistic and academic merit.
The resulting work produced a guide that followed a Maya-created film project where ZBrush was utilized in the creation of the character models, …


A Technique For Art Direction Of Physically Based Fire Simulation, Ashwin Bangalore Aug 2011

A Technique For Art Direction Of Physically Based Fire Simulation, Ashwin Bangalore

All Theses

This thesis presents an innovative way to art direct individual flames in a physically based fire simulation. Fire, due to its warm colors and constant movement, often becomes the main attraction to the viewer's eye in a scene. This technique provides control over this chaotic natural phenomenon at a microscopic level, enabling the artist to add character to flames and create highly stylized visuals. The fire system itself is a fully physics based two gas system with fuel gas and heat, with flames advected along convection currents generated by combustion. The technique is applied to examples of highly stylized flame …


Downstream Resource Allocation In Docsis 3.0 Channel Bonded Networks, Scott Moser Aug 2011

Downstream Resource Allocation In Docsis 3.0 Channel Bonded Networks, Scott Moser

All Dissertations

Modern broadband internet access cable systems follow the Data Over Cable System Interface Specification (DOCSIS) for data transfer between the individual cable modem (CM) and the Internet. The newest version of DOCSIS, version 3.0, provides an abstraction referred to as bonding groups to help manage bandwidth and to increase bandwidth to each user beyond that available within a single 6MHz. television channel. Channel bonding allows more than one channel to be used by a CM to provide a virtual channel of much greater bandwidth. This combining of channels into bonding groups, especially when channels overlap between more than one bonding …


Combining Procedural And Hand Modeling Techniques For Creating Animated Digital 3d Natural Environments, Hubert Smith Aug 2011

Combining Procedural And Hand Modeling Techniques For Creating Animated Digital 3d Natural Environments, Hubert Smith

All Theses

This thesis focuses on a systematic solution for rendering 3D photorealistic natural environments using Maya's procedural methods and ZBrush. The methods used in this thesis started with comparing two industry specific procedural applications, Vue and Maya's Paint Effects, to determine which is better suited for applying animated procedural effects with the highest level of fidelity and expandability. Generated objects from Paint Effects contained the highest potential through object attributes, texturing and lighting. To optimize results further, compatibility with sculpting programs such as ZBrush are required to sculpt higher levels of detail. The final combination workflow produces results used in the …


Open Source Rigging In Blender: A Modular Approach, Ryan Cushman May 2011

Open Source Rigging In Blender: A Modular Approach, Ryan Cushman

All Theses

Character rigs control characters in the traditional CG pipeline. This thesis examines the rig creation process and discusses several problems inherant in the traditional workflow--excessive time spent and a lack of uniformity, and proposes a software plugin which solves these issues. This thesis describes the creation of a tool for Blender 3D which automates the rigging process yet keeps the creativity and control in the hands of the user. A character rig designed by this tool will be fully functional--yet capable of being split into its component parts and reconstructed as the user determines. These body parts are individually scripted …


Stereoscopic Simulation For Animation And Special Effects, Daniel Morella May 2011

Stereoscopic Simulation For Animation And Special Effects, Daniel Morella

All Theses

Stereoscopic content, when presented well, provides an exciting and entertaining experience for viewers. The advent of new techniques and technologies is helping stereoscopy to become more commonplace, with 3D movies becoming a staple at theaters around the world. Further, 3D televisions and content are poised to experience tremendous growth in the coming years. Even video games are exploring 3D content, with recent releases like Toy Story Mania as seen on the Disney website [Disn11].
The biggest problems with stereoscopic content are that it usually requires expensive hardware to view, and extensive time and technical prowess to create. These issues limit …


Kestrel: Job Distribution And Scheduling Using Xmpp, Lance Stout May 2011

Kestrel: Job Distribution And Scheduling Using Xmpp, Lance Stout

All Theses

A new distributed computing framework, named Kestrel, for Many-Task Computing
(MTC) applications and implementing Virtual Organization Clusters (VOCs) is
proposed. Kestrel is a lightweight, highly available system based on the
Extensible Messaging and Presence Protocol (XMPP), and has been developed to
explore XMPP-based techniques for improving MTC and VOC tolerance to faults due
to scaling and intermittently connected heterogeneous resources. Kestrel provides
a VOC with a special purpose scheduler for VOCs which can provide better scalability
under certain workload assumptions, namely CPU bound processes and bag-of-task
applications.
Experimental results have shown that Kestrel is capable of operating
a VOC of …


Automated, Parallel Optimization Algorithms For Stochastic Functions, Dheeraj Chahal May 2011

Automated, Parallel Optimization Algorithms For Stochastic Functions, Dheeraj Chahal

All Dissertations

The optimization algorithms for stochastic functions are desired specifically for real-world and simulation applications where results are obtained from sampling, and contain experimental error or random noise. We have developed a series of stochastic optimization algorithms based on the well-known classical down hill simplex algorithm. Our parallel implementation of these optimization algorithms, using a framework called MW, is based on a master-worker architecture where each worker runs a massively parallel program. This parallel implementation allows the sampling to proceed independently on many processors as demonstrated by scaling up to more than 100 vertices and 300 cores.
This framework is highly …