CS Theses & Dissertations 1995

For 1995 graduation dates (in alphabetical order by last name):

SPIDER: An Agent-Based Message-Passing Architecture
Birsan, Dorian
URI : http://hdl.handle.net/2429/3761
Degree : Master of Science – MSc
Graduation Date : 1995-11
Supervisor : Dr. Wagner

Sorting Real Numbers on Random Access Machines
Blumenthal, Daniel S.
URI : http://hdl.handle.net/2429/4328
Degree : Master of Science – MSc
Graduation Date : 1995-11
Supervisor : Dr. Pippenger

Real-Time Motion Tracking: A Case Study in Parallelizing Vision Algorithms
Bulmer, Scott
URI : http://hdl.handle.net/2429/3512
Degree : Master of Science – MSc
Graduation Date : 1995-05
Supervisor : Dr. Lowe

Output-Sensitive Construction of Convex Hulls
Chan, Timothy Moon-Yew
URI : http://hdl.handle.net/2429/7188
Degree : Doctor of Philosophy – PhD
Graduation Date : 1995-11
Supervisor : Dr. Snoeyink

The construction of the convex hull of a finite point set in a low-dimensional Euclidean space is a fundamental problem in computational geometry. This thesis investigates efficient algorithms for the convex hull problem, where complexity is measured as a function of both the size of the input point set and the size of the output polytope. Two new, simple, optimal, output-sensitive algorithms are presented in two dimensions and a simple, optimal, output-sensitive algorithm is presented in three dimensions. In four dimensions, we give the first output-sensitive algorithm that is within a poly logarithmic factor of optimal. In higher fixed dimensions, we obtain an algorithm that is optimal for sufficiently small output sizes and is faster than previous methods for sublinear output sizes; this result is further improved in even dimensions. Although the focus of the thesis is on the convex hull problem, applications of our techniques to many related problems in computational geometry are also explored, including the computation of Voronoi diagrams, extreme points, convex layers, levels in arrangements, and envelopes of line segments, as well as problems relating to ray shooting and linear programming.

A VHDL Front End
Chen, Baokang
URI : http://hdl.handle.net/2429/3438
Degree : Master of Science – MSc
Graduation Date : 1995-05
Supervisor : Dr. Seger

Properties of Robot Forward Dynamics Algorithms with Applications to simulation
Cloutier, Benoit P.
URI : http://hdl.handle.net/2429/3638
Degree : Master of Science – MSc
Graduation Date : 1995-05
Supervisor : Dr. Pai

Global Garbage Detection in a Distributed Environment:  An Implementation for Raven
Devlin, Gordon
URI : http://hdl.handle.net/2429/4028
Degree : Master of Science – MSc
Graduation Date : 1995-11
Supervisor : Dr. Hutchinson

Alternative High-Performance Architectures for Communication Protocols
Jain, Parag Kumar
URI : http://hdl.handle.net/2429/3691
Degree : Master of Science – MSc
Graduation Date : 1995-05
Supervisor : Dr. Chanson

Efficiently Determing Aggregate Proximity Relationships in Spatial Data Mining
Knorr, Edwin M.
URI : http://hdl.handle.net/2429/3951
Degree : Master of Science – MSc
Graduation Date : 1995-11
Supervisor : Dr. Ng

A Simple Proof Checker for Real-Time Systems
Leung, Catherine
URI : http://hdl.handle.net/2429/3826
Degree : Master of Science – MSc
Graduation Date : 1995-11
Supervisor : Dr. Greenstreet

An Operating System Architecture for Real-Time Tasking Abstractions
Lo, Siu Ling Ann
URI : http://hdl.handle.net/2429/8868
Degree : Doctor of Philosophy – PhD
Graduation Date : 1995-05
Supervisors : Dr. Hutchinson, Dr. Chanson

A flexible real-time tasking abstraction is necessary to support diversified and evolving application-level timing constraints. Previous research has focused on rigid solutions and failed to provide any insight to a more flexible design alternative. A common approach has been to implement a real-time scheduling algorithm in the operating system kernel as an integral part of the task model. When the real-time requirements of applications evolve and a new scheduling algorithm is needed, the kernel is modified. This monolithic approach is out of step with the press for software reusability when software development and maintenance costs continue to escalate. In order to explore for a flexible design, we have examined the concepts behind existing real-time task models and classified them into competitive and cooperative task models. In contrast to the common belief that they are fundamentally different, our conclusion is that although the design of these task models are incompatible with each other, their underlying concepts are not. This paves the way for our architectural design which supports evolving real-time requirements at the application level. We propose a task abstraction where tasks cooperate and participate in making real-time scheduling decisions. This design allows for the implementation of competitive task models and their scheduling algorithms on top of a common kernel. It also provides more flexibility in task structuring since applications can be structured as cooperating tasks. We have implemented our design in the Mach 3.0 kernel and the r-kernel for experimentation and for proving the practicality of our abstraction in terms of performance and consistency with the overall design of the systems. The lessons we have learnt from implementation have strengthened our belief in the importance of providing a flexible scheduling interface which can be used by the application programmer. The flexibility of our solution is illustrated by considering the demands placed on the kernel by a modern multimedia application.

Communication Optimization in Parsec:  A parallel Programming Environment for Multicomputers
Mulye, Sameer S.
URI : http://hdl.handle.net/2429/3549
Degree : Master of Science – MSc
Graduation Date : 1995-05
Supervisor : Dr. Chanson

A Unified Recognition and Stereo Vision System for Size Assessment
Naiberg, Andrew
URI : http://hdl.handle.net/2429/5682
Degree : Master of Science – MSc
Graduation Date : 1995-11
Supervisor : Dr. Little

Transformations on Dependency Graphs:  Formal Specification and Efficient Mechanical Verification
Rajan, Sreeranga Prasannakumar
URI : http://hdl.handle.net/2429/7597
Degree : Doctor of Philosophy – PhD
Graduation Date : 1995-11
Supervisor : Dr. Joyce

Dependency graphs are used to model data and control flow in hardware and software design. In a transformational design approach, optimization and refinement transformations are used to transform dependency-graph-based specifications at higher abstraction levels to those at lower abstraction levels. In this dissertation, we investigate the formal specification and mechanical verification of transformations on dependency graphs. Among formal methods, the axiomatic method provides a mechanism to specify an object by asserting properties it should satisfy. We show that an axiomatic specification coupled with an efficient mechanical verification is the most suitable formal approach to address the verification of transformations on dependency graphs. We have provided a formal specification of dependency graphs, and verified the correctness of a variety of transformations used in an industrial synthesis frame work. Errors have been discovered in the transformations, and modifications have been proposed and incorporated. Further, the formal specification has permitted us to examine the generalization and composition of transformations. In the process, we have discovered new transformations that could be used for further optimization and refinement than were possible before. We have devised an efficient verification scheme that integrates model-checking and theorem-proving, the two major techniques for formal verification, in a seamless manner. First, we focus on the dependency graph formalism used in the high-level synthesis system part of the SPRITE project at Philips Research Labs. The transformations in the synthesis system are used for refinement and optimization of descriptions specified in a dependency graph language called SPRITE Input Language (SIL). SIL is an intermediate language used during the synthesis of hardware described using languages such as VHDL, SILAGE and ELLA. Besides being an intermediate language, it forms the backbone of the TRADES synthesis system of the University of Twente. SIL has been used in the design of hardware for audio and video applications. Next, we present schemes for seamless integration of theorem-proving and model-checking for efficient verification. We use the Prototype Verification System (PVS) to specify and verify the correctness of the transformations. The PVS specification language, based on typed higher order logic allows us to investigate the correctness using a convenient level of abstraction. The PVS verifier features automatic procedures and interactive verification rules to check properties of specifications. We have integrated efficient simplifiers and model-checkers with PVS to facilitate verification. Finally, we show how our method can be applied in the study of formalisms for hybrid/real-time systems, optimizing compilers, data-flow languages, and software engineering. Based on the applications of our method on such off-the-shelf formalisms, we substantiate our claim - that an axiomatic specification coupled with an efficient mechanical verification is the most suitable approach to specify and verify transformations on dependency graphs independent of underlying behavior models.

Aspects of Image Reshading
Romanzin, Christopher Anthony
URI : http://hdl.handle.net/2429/3560
Degree : Master of Science – MSc
Graduation Date : 1995-05
Supervisor : Dr. Fournier

Multiresolution Surface Construction for Hierarchical B-Splines
Wong, David Chak Wai
URI : http://hdl.handle.net/2429/3684
Degree : Master of Science – MSc
Graduation Date : 1995-05
Supervisor : Dr. Forsey

Performance Modelling and Evaluation of Protocols Based on Formal Specifications
Zhang, Sijian
URI : http://hdl.handle.net/2429/7470
Degree : Doctor of Philosophy – PhD
Graduation Date : 1995-11
Supervisor : Dr. Chanson

Protocol performance issues are important in communication protocol design and network management, especially for those protocols which run in high-speed networking environments. An accurate performance modelling and evaluation approach is necessary to obtain reliable performance estimations and to improve system performance. Using queueing models (QMs) or finite state machines (FSMs) alone is difficult to achieve this goal because many aspects that affect performance are not taken into consideration by the model. This thesis proposes a new performance model called performance extended finite state machine (PEFSM). PEFSM makes use of the strengths of both QM and FSM. A PEFSM is based on an FSM which is extended to include time and probability. Furthermore, the transition time is refined and divided into two parts: the transition wait time and the transition service time. This allows the PEFSMs to integrate message arrival and queueing models which provide useful and essential information necessary for studying real world protocols. PEFSMs are classified into three categories based on the message arrival characteristics: synchronous PEFSMs (SyPEFSMs), asynchronous PEFSMs (AsPEF SMs) and hybrid PEFSMs (HyPEFSMs). While the hybrid model is the most useful and realistic model for communication protocols, the other two models are also presented for completeness, and as a way to explain the hybrid model. A method for computing performance metrics based on SyPEFSMs is given in the thesis. Two types of AsPEFSMs — AsPEFSM-α and AsPEFSM-β — and their performance evaluation methods are also presented. Then a class of HyPEFSM which is a hybrid model of SyPEFSM and AsPEFSM-α is introduced. The proposed performance evaluation method for this class of HyPEFSM is basically the combination of those for SyPEFSMs and AsPEFSM-αs. Our performance mod effing and evaluation approach has been applied to various examples, including the alternating bit protocol and multi-stage interconnection network (MIN). The performance evaluation method for PEFSMs makes use of stochastic pro cess and queueing theory. A new queueing property for an M/G/1. with multiple job classes and an analogous property for AsPEFSM-os have been discovered and proved. As a first step in improving system performance, the thesis defines software performance bottlenecks based on PEFSMs. Two bottleneck identification methods are proposed and tested. This thesis also proposes a testing method called t-test which in most cases is able to obtain the service times of invisible transitions when the protocol implementation under test is given as a black box. Transition service times are important parameters in FSM-based performance models. Studies in the past have usually assumed the transition times to be known a priori without discussing how they may be obtained. Simulations and measurement experiments have been conducted to validate the methodologies proposed in this thesis. The results are quite promising.