Monday, April 28, 1997 . . . Program
3:00 PM - 5:00 PM (2:45 - 5:15 refreshments)
Third floor, Building 36
Room 34-301. 3:00 PM
Rachel Dowell
Ultrasound images display relative acoustic densities of the objects being imaged. 2D ultrasound images are routinely used in medical cardiac diagnosis. A set of 2D acquisitions obtained by rotation around an axis can be used to create a 3D image of the heart. However, movements that occur during the collection of consecutive images often produce poor reconstructions. While gating is performed on heartbeat and respiration to reduce the apparent movement between consecutive images, it does not eliminate all movement. This thesis investigates the ability of registration, using correlation as the similarity metric, to detect movement between consecutive images. Both single frame and localized correlation are investigated. Thirty-nine data pairs of tissue phantom images are used in comparing the various methods. This investigation finds that the best method uses localized correlation. The best method has a median error of 0.7 pixels and has only one case of failure in the 39 data pairs.
Supervisors: Prof. Tomás Lozano-Pérez; Bob Arling; Stockton Miller-Jones, Hewlett-Packard
Michael E. Leventon
Medical scans such as Magnetic Resonance (MR) and computed tomography (CT) are currently common diagnostic tools in surgical applications. Typically information contained in these medical scans is neither in the coordinate system of the patient as positioned in the world, nor does it reflect the viewpoint of the surgeon during an operation. Any correspondences between the medical images and the actual patient environment have to be drawn mentally by the surgeon during the procedure. The approach of medical image registration seeks to compute these correspondences automatically and then directly augment the real operating environment with the information contained in medical scans. In this talk, I will describe work we have done designing and building augmented reality environments for various types of medical procedures, including neurosurgery, functional brain mapping, and endoscopic intubation. Such environments provide the surgeon with an enhanced ability to plan, navigate and localize throughout a surgical procedure.
Supervisor: Prof. W. Eric L. Grimson
Ruilin Zhao
With the proliferation of modern monitoring and laboratory procedures, physicians in intensive care areas may face "information overload," in dealing with very large, complex and ever-changing quantities of clinical data, which often lacks efficient organization. This research analyzes the medical knowledge required for formulating decision models in the domain of hemodynamics. Based on such analysis, a knowledge based expert system to track a patient's hemodynamic state is developed. Given observable hemodynamic data, such as arterial blood pressure, etc., together with additional data from patient history and other lab tests, the expert system automatically assigns values to the parameters of a cardiovascular model such that the model output matches the patient data. Several pathological simulations have been successfully analyzed by this expert system, including hypertension, heart failure, etc. We conclude that our approach is practical, and provides a mechanism for transforming and reducing real-time physiologic data into pathophysiologic hypotheses relevant to the management of patients.
Supervisors: Prof. Roger G. Mark; Prof. Peter Szolovits
Room 34-302. 3:00 PM
Gilbert Leung
Synthetic aperture radars (SARs) provide the coverage rate and all-weather operability needed for wide-area surveillance. SAR-based automatic target recognition (ATR) systems need fast and effective discriminators to suppress vast amounts of natural clutter from, while admitting the much more limited set of man-made object data to, their classification processors. The different physical behaviors of the scattering of man-made targets and natural clutter give specular and diffuse reflections, which motivate this work to use a physical optics formalism to establish a first-principle analysis for discriminating specular returns from diffuse returns in a 1-D SAR. The optimal Neyman-Pearson detection processor, one that maximizes the probability of detection given a desired probability of false alarm, is shown to substantially outperform the conventional SAR imager for extended specular targets embedded in diffuse clutter plus receiver noise. Significant performance advantages, relative to conventional SAR processing, are also shown to accrue for optimum Neyman-Pearson reception of an extended diffuse target embedded solely in receiver noise.
Supervisor: Prof. Jeffrey H. Shapiro
Yin-Chun Andrew Kao
There is tremendous interest in the application of Finite-Difference Time-Domain method to study the frequency filtering behaviors of the periodic surfaces. However, past efforts at applying the technique to periodic surfaces have been limited to normal incidence, plagued by instability problems, or constrained to single frequency excitation due to the breakdown of the periodic side boundary condition at oblique incidence. This thesis investigates a method of overcoming this difficulty via the substitution of new field quantities for electric and magnetic fields. The new quantities restore the validity of the periodic boundary condition. Changes to the standard FD-TD algorithm needs to be made as well, including more complicated propagation expressions, alternate lattice structure, generalized stability criterion, and modifications to the absorbing boundary condition. The algorithm is implemented and verified for the computation of scattering characteristics of geometries that include lossless dielectric, lossy dielectric, and perfect conductors at various incidence angles.
Supervisors: Robert G. Atkins, MIT Lincoln Laboratory; Prof. Jin Au Kong
Jeffrey Roth
The modulation of optical carriers by radio frequency (RF) and microwave signals has proven to be a promising means of fulfilling needs in the analog realms of antenna remoting, common antenna television (CATV), phased array radar element control, and cellular communication links. Among the many techniques used in analog fiber links, intensity modulation has been most widely investigated for both direct and external modulation links. Limitations on noise figure and dynamic range have recently led people to pursue the use of optical frequency modulation (FM) links. Our goal is to take advantage of feedback to demodulate an optical FM signal through a electro-optically tuned Mach-Zehnder interferometer. The bandwidth of the receiver can be increased by a fixed path length difference introduced in the interferometer, thereby enhancing the sensitivity, and gain, of the demodulator. We will discuss the progression of work on this direct detection optical FM link by showing measurements on gain, noise figure, and dynamic range, and comparing these values to what has been attained with other direct detection links.
Supervisors: Prof. James K. Roberge; Dr. Charles H. Cox, III, MIT Lincoln Laboratory
Room 34-303. 3:00 PM
Aarati Parmar
This Master's Thesis concerns the automatic analysis of the sublexical structure of English words. This structure includes linguistic categories such as syllabification and stress. This information could be useful in many speech applications, including duration modeling and recognition. ANGIE is a system that can parse either the phonetics or spelling of a word into a common hierarchical framework with the above categories, which allows it to perform automatic sound-to-letter or letter-to-sound generation. ANGIE is trained from a large lexicon of words, each represented as a sequence of "morph" units, each of which is in turn represented by a phonemic realization. The morph units encode both the orthography and the phonemics of the word. This thesis defines a procedure to semi-automatically absorb new words into ANGIE's lexicon, producing morph sequences for the words. Both phonetics and spelling information are used to confirm validity. Words which fail to parse are interesting since they show the framework's generality. They also provide new information about the sublexical structure of English.
Supervisors: Stephanie Seneff, Principal Research Scientist; Helen Meng, Research Scientist
Sridevi Sarma
Speaker verification involves the task of automatically verifying a person's identity by his/her speech through the use of a computer. This thesis describes the development of a segment-based speaker verification system. Our investigation is motivated by past observations that speaker-specific cues may manifest themselves differently depending on the manner of articulation of the phonemes. By treating the speech signal as a concatenation of phone-size units, one may be able to capitalize on measurements for such units more readily. A potential side benefit of such an approach is that one may be able to achieve good performance with unit (i.e., phonetic inventory) and feature sizes that are smaller than what would normally be required for a frame-based system, thus deriving the benefit of reduced computation.We tested 168 speakers and were able to achieve a performance of 0% false rejection of true users and 4.85% false acceptance of impostors. Our system design is very simple and we reduced computation significantly through the use of a small number of features, a small number of phonetic models per speaker, few model parameters, and few competing speakers during testing.
Supervisor: Dr. Victor Zue, Senior Research Scientist
Sumit Basu
In the course of ordinary conversation and expression, the human lips can deform in a variety of interesting and non-rigid ways. Tracking these motions accurately has proved to be quite difficult. I propose that with an accurate model of the lips, this task will be greatly simplified. In essence, the argument is that a model that can only vary in the ways that the lips actually move will not be "fooled" by erroneous data. In this study, I present a 3D model of human lips and develop a framework for training it from real data. The model starts off with generic physics specified with the finite element method and "learns" the correct variations through observations. The model's physics allow physically-based regularization between sparse observation points and the resulting set of deformations are used to derive the correct physical modes of the model. Preliminary results showing the model's ability to reconstruct lip shapes from sparse data are shown. The resulting model can be used for both analysis and synthesis.
Supervisor: Prof. Alex Pentland
Room 34-304. 3:00 PM
Leong, Ben W.
Networks for powering broadband (fiber optic or coaxial cable) systems are becoming more common as the consumer's demand for more bandwidth to the home has been steadily rising. Unfortunately, very little analytical work has so far been done on the dynamic behavior and stability properties of such power networks in the literature. A better understanding of their properties can lead to better designs and possibly substantial monetary savings. This thesis presents the results of a study into the static and dynamic properties of broadband power networks. An RC-tree is used to model the network itself, and a constant-power (P) model is used to represent the load at each node of the network. A general method to convert the resulting model into a gradient system representation is presented. Properties of gradient systems are then exploited to obtain insight into the dynamic behavior of the system. Various conditions for stability (including simple sufficient conditions) are derived. An approximation approach to computing the static equilibria of such networks is also developed.
Supervisor: Prof. George C. Verghese
Andrew J. Kim
There has recently been a growing interest in Synthetic Aperture Radar (SAR) imaging on account of its importance in a variety of applications. One reason for its gain in popularity is its ability to image terrain at extraordinary rates. Acquiring data at such rates, however, has drawbacks in the form of exorbitant costs in data storage and transmission. To abate these and related costs, we propose a segmentation driven compression technique using hierarchical stochastic modeling within a multiscale framework. Our approach to SAR image compression is unique in that we exploit the multiscale stochastic structure inherent in SAR imagery. This structure is well captured by a set of scale auto-regressive (AR) models that accurately characterize the evolution in scale of homogeneous regions for different classes of terrain. We thus use them to generate a multiresolution segmentation of the image. We subsequently use the segmentation in tandem with the corresponding models to provide a robust, hierarchical compression technique which in addition to coding the segmentation, codes the image with impressive quality.
Supervisor: Hamid Krim, Research Scientist
Matthew Secor
In this talk, I will discuss optimal resource allocation in certain classes of networks of interconnected approximate processors. An approximate processor is one that allows tradeoffs between the quality of the results and the resource usage of the processor. Previous work with anytime algorithms and incremental refinement structures is used to motivate and develop a method of modeling the quality tradeoffs for approximate processors and networks, extending earlier models. I will review methods developed previously for compiling anytime algorithms in which the quality of the output of the network is optimized, subject to some set of resource constraints. These algorithms are then extended --- for particular types of networks --- to apply in a more general situation in which the component processors of a network may be physically distributed and have multiple associated quality measures.
Supervisor: Prof. George Verghese
Room 34-401A. 3:00 PM
Van C. Van
This thesis studies a prevalent denial-of-service attack known as SYN-Flooding and presents a possible defense using active network technology. This type of attack uses spoofed Internet addresses to exploit a weakness in the 3-way handshake employed by the Transmission Control Protocol (TCP). It can easily render a server relatively inaccessible to legitimate users or even bring a server down completely. As yet, there is no "generally" accepted solution for this problem in today's network environment. Active networks, which provide increased computational power within the network itself, have recently been proposed as a means of deploying new network applications and of performing application-specific computation within the network. This computational power can also be used to deter denial-of-service attacks. I have built a prototype dynamic filter that can be deployed when an attack is suspected to filter out forged packets within the network. Currently the filter only works in networks that use symmetric routing. I am working on relaxing this constraint to make the filter work in a less restrictive environment.
Supervisor: Stephen J. Garland, Principal Research Scientist
David Murphy
Today's Internet Protocol (IP) networks contain nodes that process packets according to a set of predefined specifications that enable all nodes to interoperate. Because of this, deploying protocol upgrades, or even new protocols, is a slow and difficult process, requiring years of proposals, evaluation committees, and testing. Active Network research has begun to address this problem by defining an alternative network architecture in which applications can dynamically deploy new protocols. As packets pass through nodes within this architecture, they select the protocol by which they are to be processed. This talk will present the design and implementation of a node that combines both IP and Active Network functionality. It utilizes the next generation IP protocol, IPv6. This node can route "traditional" Ipv6 packets, and execute programming code embedded in "non-traditional" Active IPv6 packets. Further, it can coexist in the same IPv6 network with other IPv6 nodes that may or may not support Active Network functionality. This characteristic makes the node a useful platform on which to study the capabilities of application-specific protocols that use a heterogeneous network containing Active and non-Active IPv6 nodes.
Supervisors: Prof. John V. Guttag; David L. Tennenhouse
Paolo L. Narvaez Guarnieri
Flow control is a regulation policy which limits the source rates of a network so that the network is well utilized while minimizing traffic congestion and data loss. The difficulties in providing an effective flow control policy are caused by the burstiness of data traffic, the dynamic nature of the available bandwidth, as well as the feedback delay. This thesis develops analytical tools for designing efficient flow control algorithms in data networks. Using a control theoretic framework, this thesis proposes a new design methodology for congestion control algorithms based on separating the problem into two simpler components: rate reference control (RRC) and queue reference control (QRC). The RRC component matches the input rate of a switch to its available output bandwidth, while the QRC component maintains the queue level at a certain threshold and minimizes queue oscillation around that threshold. Separating the flow control problem into these two components decouples the complex dynamics of the system into two easier control problems which are analytically tractable. A specific flow control algorithm which uses these ideas is presented. The algorithm is provably stable and has the shortest possible transient response time. Moreover, it achieves fair bandwidth allocation among contending connections and maximizes network throughput.
Supervisor: Prof. Kai-Yeung Siu
Room 34-401B. 3:00 PM
Alexander N. Ernst
InAlAs/InGaAs/InP High Electron Mobility Transistors (HEMTs) show significant promise for high-power millimeter-wave applications. A significant anomaly in their output characteristics is the kink-effect, a sudden rise in drain current at a certain drain-to-source voltage that results in non-linear drain conductance and gain compression. The physical origin of the kink is not understood. We are attempting to shade light to it by studying its dynamics under pulsed operation. In this work we have carried out the first nanosecond-range dynamic study of the kink effect in InAlAs/InGaAs/InP HEMTs by means of a specially designed pulsed I-V setup. Our results indicate that the kink build-up characteristic time constant (T90%) is strongly dependent on the operating bias. For example, T90% is seen to drop by more than three decades, from 100 ms down to 50 ns for 1 < VDS < 2.1 V. Our results are consistent with the barrier-induced hole pile-up theory presented by Somerville et al. (in IEDM '95). This theory postulates that the kink is due to conductivity modulation at the source-end of the device. Essentially, impact ionization (II) generated holes at the drain end of the device drift to the source where they pile-up. This hole pile-up increases the local electron concentration, leading to a reduction in source resistance and thus extra gate voltage. Our experiments also confirm the correlation between the kink and II and show that the kink is not present at frequencies beyond 1 GHz.
Supervisor: Prof. Jesús del Alamo
Christopher S. Putnam
InGaAs/InAlAs High Electron Mobility Transistors (HEMTs) show promise as mm-wave power devices. While increasing their breakdown voltage (BV) is essential for improving power performance, the physics of BV was not well known and no predictive model was available until recently. New research suggests tunneling and thermionic-field emission (TFE) as the dominant mechanism for BV. A model for tunneling-limited BV was presented, but there has been no extension to include TFE. We have done extensive characterization on a large sample of state-of-the-art HEMTs. Our results support the tunneling/TFE model. With the gate Schottky barrier height (phiB) constant across the sample, we observe that BV is inversely related to ns but there is no significant dependence on other parameters, just as the model predicts. Using values extracted for phiB and ns (given by the grower), we were able to calculate the gate current (IG) and BV. The theory matches well the measured IG near both temperature extremes. Furthermore, the theory correctly predicts the negative temperature dependence and even closely predicts the actual values of the breakdown voltage.
Supervisor: Prof. Jesús del Alamo
Room 34-301. 4:00 PM
Ruben Agin
A cellular automaton (CA) is an array of identical, locally interconnected processors called cells, each of which is updated synchronously and in parallel by a uniform rule that depends only on the states of nearby neighboring cells. This is essentially a gate array with a fixed neighborhood interconnect pattern. CAM-8 (a cellular automata machine) is a scalable machine that simulates CA in a virtual manner: by time- sharing each processor over a "chunk" of space, one also time-shares the wires interconnecting the chunks, greatly reducing wiring problems (particularly in 3-D), and greatly increasing the ratio of gates used for processing to gates used for state. In addition, combinational latency is reduced to one update of the space. The objective of this thesis is to demonstrate how CAM-8 can be used to perform logic simulations efficiently and investigate the appropriate synthesis techniques. Several benchmark circuits, including a microprocessor have already been successfully laid out and simulated. This talk will discuss some of the issues mentioned above, what has been implemented, the results that have been obtained so far, and what has been learned.
Supervisor: Norman Margolus, Visiting Scientist
Cristina Hristea
As more sophisticated techniques are used in modern microprocessors to optimize program performance, and in particular to hide and reduce memory latency, measuring memory performance has become increasingly difficult. In shared-memory multiprocessors this task is complicated even more so by cache coherency and contention. First, this thesis analyzes the components of memory performance. Secondly, it presents a micro benchmark suite which measures these components by handling both sophisticated processor optimizations and multiprocessor workloads. Finally, it describes the applicability of the suite using concrete examples and results.
Supervisors: John Keen, MTS, SGI; Prof. Arvind
Jimmy S. Shih
The thesis objective is to design an autonomous spacecraft architecture to perform both deliberative and reactive behaviors. The Autonomous Small Planet In-situ Reaction to Events (ASPIRE) project uses this architecture to integrate several autonomous technologies for a comet orbiter mission. This architecture uses the deliberative path for performing deliberative behaviors, and the three bypass paths for performing reactive behaviors. The deliberative path subsumes the three bypass paths when it has time to handle events. The three bypass paths are used to provide faster response time. The ASPIRE project shows that the deliberative path can handle all the deliberative behaviors required by the mission, although, the three bypass paths for handling reactive behaviors are not implemented in the project. Finally, this thesis describes several good design and implementation elements.
Supervisors: Prof. Patrick H. Winston; Prof. Arvind
Room 34-302. 4:00 PM
Laura Johnson
We have developed a method to characterize the motions of MEMS that combines video microscopy and computer vision to estimate 3-D motions with nanometer precision. To test these methods, I have studied a microfabricated angular rate sensor (gyroscope) from Draper Laboratory. The gyroscope is driven to vibrate in the plane of the structure, and it senses out-of-plane motions. Out-of-plane motions induced during rotation are proportional to the gyroscope's angular velocity. Both in-plane and out-of plane motions have been analyzed. To demonstrate these results, I will show quantitative analyses and slow motion video sequences of the moving gyroscope. A 3-D frequency response of the gyroscope demonstrating both in-plane and out-of-plane resonances will be discussed. In addition, out-of-plane levitation and rocking modes of motion can be excited using different stimuli. Out-of-plane motions are of particular interest because they affect the sensitivity of the gyroscope.
Supervisors: Quentin Davis; Prof. Dennis Freeman
Wendi Beth Rabiner
Due to the massive amount of data contained in video signals and the limited bandwidth of the wireless channel, compression techniques for these applications are extremely important. Conventional video systems use some form of scene motion estimation/motion compensation at the encoder to reduce the temporal correlation inherent in most video signals and hence achieve high compression ratios. However, since most motion estimation algorithms require a large amount of computation, it is undesirable to use them in power constrained applications, such as battery operated wireless video terminals. Minimizing power dissipation is the key to maximizing battery lifetime and thus should be one of the driving forces when designing motion estimation algorithms for portable video encoders. We have developed an approach to reducing the power dissipation of wireless video terminals in a networked environment by exploiting the predictability of object motion. Since the location of an object in the current frame can be predicted from its location in previous frames, it is possible to optimally partition the motion estimation computation between battery operated portable devices and high powered compute servers on the wired network.
Supervisor: Prof. A. P. Chandrakasan
Dewey S. Tucker
The classical estimation problem, namely estimating an unknown signal in additive noise, has recently been revisited by researchers. Wavelets and wavelet packets can be attributed to the resurgence of interest in this area. One of the most significant properties of wavelets, which we exploit, is their ability to represent signals in a given smoothness class with very few large magnitude coefficients. In this research, we find an "optimal" representation of a given signal in a wavelet packet tree, such that removing noisy coefficients at a given threshold improves the signal quality and minimizes the error in reconstructing the signal.
Supervisor: Dr. Hamid Krim
Room 34-303. 4:00 PM
Prasanna Tambe
This report describes a system to extract three dimensional facial motion data from video recordings that include multiple camera angles of a speaker's face. The face is marked to allow easy identification of corresponding points between frames. On an initial frame, the user selects matching points from the different camera perspectives. The user also locates several reference points to set scaling parameters. Active contours track these points through subsequent frames, using edge detection and energy minimizing methods to "lock-on" to features. The displacement of the selected points in the different views is measured, correlated, and converted into three dimensional coordinates.
Supervisors: Joe Frisbie; Prof. Lou Braida
Erik G. Miller
In this talk, we first review local counting methods for perimeter estimation of piecewise smooth binary figures on square and hexagonal grids. We verify that better perimeter estimates can be obtained on a hexagonal grid. We then compare surface area estimates using local counting techniques for binary three-dimensional volumes under three distinct tilings: the cubic, truncated octahedral, and rhombic dodecahedral tilings. It is shown that under certain assumptions of piecewise smoothness, the mean error of surface area estimates is smaller for the truncated octahedral and rhombic dodecahedral tilings than for the standard cubic or rectangular prism tilings of space. Additional properties of these tessellations are reviewed and potential applications of better surface area estimates are discussed.
Supervisor: Prof. Berthold K. P. Horn
Chris Stauffer
Standard scene reconstruction methods attempt to determine the positions which visible elements of the environment occupy in space. Instead of determining where things are, I choose to model where things are not. I model the open space in a scene. This is accomplished by tracking a human participant moving in the environment. Based on where the tracked object is and where it is visible to the cameras, a 3-D vacancy grid is modified which represents the empty space in the environment. This method can produce useful spatial models itself or can be used to complement other reconstruction methods.
Supervisor: Prof. W. Eric L. Grimson
Room 34-304. 4:00 PM
Steven R. Shaw
Three methods for determining the parameters of a lumped induction motor model given stator current and voltage measurements during a startup transient will be presented. The first method extrapolates a series of biased estimates obtained from reduced order models to an unbiased estimate. The second method uses part of the model as a rotor current estimator. The estimated rotor currents are used to predict rotor voltage errors, which are then minimized. The third method, developed in a more general context and applied to the specific case of the induction motor, finds parameters of a possibly non-linear differential equation. The identification methods are tested using simulated and measured transient data.
Supervisor: Prof. Steven B. Leeb
Mathew Varghese
The use of capacitance measurement to determine the position of an elastically supported plate is limited by the phenomenon known as pull-in. Recently, a dynamic differential capacitive sensing scheme was proposed that uses voltages much higher than the pull-in voltage. Short pulses that exceed the pull-in voltage are applied differentially to a sense capacitor and reference capacitor. The voltage that appears on their shared node during the sense pulse is proportional to the difference between the two capacitances. Because the pulses are applied for a very short time, static pull-in does not occur. However, the pulses impart kinetic energy to the supported plate and the mechanical system can undergo oscillatory motion. This motion must be controlled in amplitude, and must be optimally damped so that the next sense measurement can be made as quickly as possible. This thesis investigates the electromechanical dynamics of both the sense procedure and a proposed resistive damping method that permits effective damping even for devices that must operate in vacuum, and hence, cannot depend on squeeze-film damping. Resistive damping couples the electrostatic and mechanical energy domains and damps by dissipating energy through Joule heating in a resistor. A 1-D model of a thermo-mechanical radiant energy sensor is used to illustrate the sensing and damping dynamics, and show how parameters for optimal damping can be found.
Supervisor: Prof. S. D. Senturia
Danielle Coffing
A design method for switching regulators using Matlab and Simulink has been developed. The Matlab script presented calculates the necessary bandwidth of the loop given the power distribution network characteristics and the maximum acceptable output voltage variation. The compensation network is then calculated for given characteristics of the output filter components. The script also analyzes the stability over the range of possible load currents. The transfer functions describing the system are loaded into a regulator model in Simulink so that transient simulations can be performed. This design method has been correlated with Spice and four breadboards. The design cycle time can be decreased by using Matlab to gain intuition for how parameter and component variation affect the stability and transient performance of the regulator. This method presented is then used to determine the necessary characteristics of the error amplifier and comparators used in the MC33470 design. Finally, the OTA and comparator designs are presented.
Supervisors: Robert Vyne, Motorola; Prof. Martin F. Schlecht
Room 34-401A. 4:00 PM
Roberto De Prisco
This thesis develops a new I/O automaton model called the Clock General Timed Automaton (Clock GTA) model. The Clock GTA is based on the General Timed Automaton (GTA) of Lynch and Vandraager. The Clock GTA provides a systematic way of describing timing-based systems in which there is a notion of "normal" timing behavior, but that do not necessarily always exhibit this "normal" behavior. It can be used for practical time performance analysis based on the stabilization of the physical system. We use the Clock GTA automaton to model, verify and analyze the Paxos algorithm. The Paxos algorithm is an efficient and highly fault-tolerant algorithm, devised by Lamport, for reaching consensus in a distributed system. Although it appears to be practical, it is not widely known or understood. This thesis contains a new presentation of the Paxos algorithm, based on a formal decomposition into several interacting components. It also contains a correctness proof and a time performance and fault-tolerance analysis.
Supervisor: Prof. Nancy A. Lynch
Carolos Livadas
This thesis investigates how the formal modeling and verification techniques of computer science can be used for the analysis of hybrid systems --- systems involving both discrete and continuous dynamics. The motivation behind such research lies in the inherent similarity of the hierarchical and decentralized control strategies of hybrid systems and the formal techniques used for the verification of distributed systems in computer science. As a case study, the thesis focuses on the development of techniques that use hybrid I/O automata to model and analyze automated vehicle transportation systems and their various protection subsystems. The thesis is split into two major parts. First, we develop an abstract model of a physical plant that is interacting with several protection subsystems. Second, we specialize the abstract models to simplified versions of the personal rapid transit system under development at Raytheon Corporation and its protection subsystems that guarantee that the vehicles comprising the physical plant neither exceed a prespecified speed limit, nor collide among themselves.
Supervisor: Prof. Nancy A. Lynch
Kevin K. Lin
This project investigates the computational representation of manifolds, which are mathematical abstractions that help manage multiple coordinate systems on n-dimensional analogs of curves and surfaces. Using this abstraction, one can accurately integrate ordinary differential equations, particularly those arising from classical mechanics, over multiple coordinate systems. One can also apply this abstraction to the numerical solution of simple linear partial differential equations, such as Laplace's equation or the linear wave equation, although in this case unexpected difficulties arise even with simple equations.
Supervisor: Prof. Gerald Jay Sussman
Room 34-401B. 4:00 PM
Yang-hua Chu
Digital signatures alone are not sufficient for code signing and other applications: signatures can solve the problems of message integrity and authentication, but not more general notions of security or trust. These applications require not only cryptographic tools for determining authenticity and message integrity but also a mechanism that permits users to clearly state their own security policies and evaluate digital signatures with respect to those policies. For example, in a code signing application a user must state under what conditions they trust the code. Similarly, the entity signing the code must state precisely what properties they claim the code has (e.g. virus-free, works with particular hardware platforms). This presentation will identify what 'trust management' is in the context of the World Wide Web and propose an architecture to close the gap between web users and cryptography. I will describe both a specific language for describing trust policies and a general mechanism for evaluating them.
Supervisors: Jim Miller, MIT/W3C; Joan Feigenbaum, AT&T
Nimisha Mehta
Lurking in web pages, mobile codes are automatically executed on the client's machine. Java applets are such examples which, with their popularity and scalability, can easily damage naive users' computer systems. As a result, popular Web browsers are quite conservative on what they allow Java applets to do. However, this places a heavy restriction on applets which drastically limits their capabilities. Therefore, we have developed a constraint language in which naive users can specify their fine-grained control over applets without needing to know the Java language nor the intricacies of applet security. We have written an implementation of the Java Security Manager built into Netscape and Sun's AppletViewer to demonstrate the feasibility and success of this approach, addressing the many security issues that arise when opening the operating system to the public domain. This involves maintaining a log of applets' past accesses to determine the allowability of their future accesses, along with an account of which applets "own" which files.
Supervisor: Dr. Karen Sollins, Research Scientist, LCS
Jennifer Ching-Wen Han
My project includes researching and designing a system dynamics model for use in an existing project management training game. This serves two major purposes. The first is to show how system dynamics can be used as a realistic and potentially superior method of business modeling. The second is to actually improve the existing game. The current training game leads trainees through managing a project via a series of case studies. With each case study, trainees analyze and discuss why certain parameters are unrealistic and how they would change them. Parameters include the amount of time spent on testing, head count, and expected completion date. Each following case, however, will continue the project using the unrealistic parameters rather than the corrections noted by the trainees. The improved game will include a computerized system dynamics model so that trainees will be able to input their own parameters rather than continuing the project using suboptimal numbers.
Supervisors: Prof. Richard Larson; Prof. Steven Lerman; Prof. John Sterman
|
Modified: Jun 24, 1997|
Current events|
Your comments
and inquiries are welcome.