Open Access. Powered by Scholars. Published by Universities.®
- Discipline
-
- Physical Sciences and Mathematics (825)
- Computer Engineering (733)
- Computer Sciences (730)
- Mechanical Engineering (376)
- Biomedical Engineering and Bioengineering (211)
-
- Electrical and Computer Engineering (127)
- Chemical Engineering (88)
- Life Sciences (76)
- Materials Science and Engineering (62)
- Civil and Environmental Engineering (53)
- Bioimaging and Biomedical Optics (51)
- Environmental Engineering (51)
- Electrical and Electronics (49)
- Physics (47)
- Aerospace Engineering (42)
- Medicine and Health Sciences (35)
- Engineering Science and Materials (34)
- Optics (34)
- Mechanics of Materials (30)
- Chemistry (26)
- Nanoscience and Nanotechnology (25)
- Aerodynamics and Fluid Mechanics (24)
- Neuroscience and Neurobiology (24)
- Molecular, Cellular, and Tissue Engineering (17)
- Biochemistry, Biophysics, and Structural Biology (16)
- Biomedical (16)
- Artificial Intelligence and Robotics (15)
- Medical Specialties (15)
- Applied Mathematics (14)
- Keyword
-
- CFD (17)
- Machine learning (17)
- Optimization (16)
- Machine Learning (11)
- Microfluidics (10)
-
- Fluorescence (9)
- Imaging (9)
- Mems411 (9)
- Biomaterials (8)
- Cancer (8)
- FPGA (8)
- Image reconstruction (8)
- Polarization (8)
- Aerosol (7)
- Biomechanics (7)
- Cyanobacteria (6)
- Deep Learning (6)
- Deep learning (6)
- Lignin (6)
- Mechanobiology (6)
- Nanoparticles (6)
- Nucleation (6)
- Acoustofluidics (5)
- Computational Fluid Dynamics (5)
- Computational imaging (5)
- Computed tomography (5)
- Control (5)
- Focused ultrasound (5)
- Metabolic Engineering (5)
- Metabolic engineering (5)
- Publication Year
- Publication
-
- McKelvey School of Engineering Graduate Student Theses & Dissertations (783)
- All Computer Science and Engineering Research (683)
- Mechanical Engineering Design Project Class (242)
- Washington University / UMSL Mechanical Engineering Design Project JME 4110 (40)
- All Theses and Dissertations (ETDs) (36)
-
- Electrical & Systems Engineering Publications and Presentations (23)
- Computer Science and Engineering Faculty Research (3)
- Electrical and Systems Engineering Capstone Design Projects (3)
- Generative AI Teaching Activities (3)
- Undergraduate Research Symposium Posters (3)
- Olin Business School Graduate Student Theses and Dissertations (2)
- Books and Monographs (1)
- Doctor of Business Administration Dissertations (1)
- ENGR 310: Technical Writing Final Project (1)
- Graduate School of Architecture & Urban Design Theses & Dissertations (1)
- Mathematics Faculty Research (1)
- Senior Honors Papers / Undergraduate Theses (1)
- WashU Libraries Presentations (1)
- Publication Type
- File Type
Articles 1471 - 1500 of 1828
Full-Text Articles in Engineering
Multiflow Tcp, Udp, Ip, And Atm Traffic Generation Module, Eliot I. Sinclair, John W. Lockwood
Multiflow Tcp, Udp, Ip, And Atm Traffic Generation Module, Eliot I. Sinclair, John W. Lockwood
All Computer Science and Engineering Research
Networking devices must be capable of processing traffic flows from multiple sources. In order to verify that such devices operates properly, a network testbench can be used to inject traffic into the device. The specification of the traffic flows can be difficult. At the low level, there are header fields, data checksums, and packet length fields that all must be formatted correctly. Further, there can be multiple flows of traffic that will arrive simultaneously. It is desirable to specify traffic at a high level of abstraction. A software program can then be written to parse the specification and generate the …
System-On-Chip Packet Processor For An Experimental Network Services Platform, David Taylor, Alex Chandra, Yuhua Chen, Sarang Dharmapurikar, John Lockwood, Wenjing Tang, Jonathan Turner
System-On-Chip Packet Processor For An Experimental Network Services Platform, David Taylor, Alex Chandra, Yuhua Chen, Sarang Dharmapurikar, John Lockwood, Wenjing Tang, Jonathan Turner
All Computer Science and Engineering Research
As the focus of networking research shifts from raw performance to the delivery of advanced network services, there is a growing need for open-platform systems for extensible networking research. The Applied Research Laboratory at Washington University in Saint Louis has developed a flexible Network Services Platform (NSP) to meet this need. The NSP provides an extensible platform for prototyping next-generation network services and applications. This paper describes the design of a system-on-chip Packet Processor for the NSP which performs all core packet processing functions including segmentation and reassembly, packet classification, route lookup, and queue management. Targeted to a commercial configurable …
A Thesis On A 3d Input Device For Sketching Characters, Mark A. Schroering
A Thesis On A 3d Input Device For Sketching Characters, Mark A. Schroering
All Computer Science and Engineering Research
The goal of this project is to develop a 3D input device using a stiff piece of paper and a camera. The camera tracks the piece of paper in 3D space. The user orients the paper in 3D space and then draws on the paper using a pen-like device. The camera tracks the movement of the pen on the piece of paper. The location of the pen in 3D space can then be calculated from the orientation of the paper. A drawing application that uses this 3D input device was also developed. The application allows a user to make characters …
A Study In Java Bytecode Engineering With Pcesjava, Martin R. Linenweber
A Study In Java Bytecode Engineering With Pcesjava, Martin R. Linenweber
All Computer Science and Engineering Research
This thesis reports on experience with PCESjava, a collection of tools which we have developed for the purpose of aiding programmers. Particular applications optimize and instrument JAVA bytecode programs. Using these tools, we have successfully identified impediments to real-time performance in a popular JAVA collections object. Our approach here is based on automatic instruction to obtain traces that show paths whose execution time is not reasonably bounded. We also report on the application of our tool to reduce program footprint in JAVA programs by rewriting the bytecodes to occupy less space. Our transformations also improves the running time of set …
An Iterative Loop Matching Approach To The Prediction Of Rna Secondary Structures With Pseudoknots, Jianhua Ruan, Weixiong Zhang
An Iterative Loop Matching Approach To The Prediction Of Rna Secondary Structures With Pseudoknots, Jianhua Ruan, Weixiong Zhang
All Computer Science and Engineering Research
Motivation: Pseudoknots have generally been excluded from the prediction of RNA secondary structures due to the difficulty in modeling and complexity in computing. Although several dynamic programming algorithms exist for the prediction of pseudoknots using thermodynamic approaches, they are neither reliable nor efficient. On the other hand, comparative methods are more reliable, but are often done in an ad hoc manner and require expert intervention. Maximum weighted matching (Tabaska et. al, Bioinformatics, 14:691-9, 1998), an algorithm for pseudoknot prediction with comparative analysis, suffers from low prediction accuracy in many cases. Here we present an algorithm, iterative loop matching, for predict-ing …
Towards A Performance Model For Special Purpose Orb Middleware, Venkita Subramonian, Guoliang Xing, Christopher Gill, Ron Cytron
Towards A Performance Model For Special Purpose Orb Middleware, Venkita Subramonian, Guoliang Xing, Christopher Gill, Ron Cytron
All Computer Science and Engineering Research
General purpose middleware has been shown effective in meeting diverse functional requirements for a wide range of distributed systems. Advanced middleware projects have also supported single quality-of-service dimensions such as real-time, fault tolerance, or small memory foot-print. However, there is limited experience supporting multiple quality-of-service dimensions in middleware to meet the needs of special purpose applications. Even though general purpose middleware can cover an entire spectrum of functionality by supporting the union of all features required by each application, this approach breaks down for distributed real-time and embedded sys-tems. For example, the breadth of features supported may interfere with small …
Twinscan: A Software Package For Homology-Based Gene Prediction, Paul Flicek
Twinscan: A Software Package For Homology-Based Gene Prediction, Paul Flicek
All Computer Science and Engineering Research
A complete mapping from genome to proteome would constitute a foundation for genome-based biology and provide targets for pharmaceutical and therapeutic intervention. This is one reason gene structure prediction has been a major subfield of computational biology for over 20 years. Many of the widely used gene prediction systems were developed in the 1990s and are unable to take advantage of the revolution in comparative genomics brought on by the sequencing of the entire genomes of an increasing numbers of vertebrates. Twinscan is a new system for high-throughput gene-structure prediction that exploits the patterns of conservation observed in alignments between …
Storage Allocation In Bounded Time, Sharath Reddy Cholleti
Storage Allocation In Bounded Time, Sharath Reddy Cholleti
All Computer Science and Engineering Research
The correctness of a real-time system is very much dependent on the time at which a specific task is completed. Hence, satisfying a storage allocation request within bounded time is important. Fragmentation of the heap after repeated allocations and deallocations is a major issue for real-time systems, as most allocators depend on garbage collection for defragmentation of the heap, which might not finish in time to honor deadlines. We present the storage requirement for a defragmentation-free binary-buddy allocator. We also study a localized defragmentation algorithm to satisfy a single allocation request, within bounded time, instead of requiring defragmentation of the …
The Design And Performance Of Special Purpose Middleware: A Sensor Networks Case Study, Venkita Subramonian, Guoliang Xing, Christopher Gill, Ron Cytron
The Design And Performance Of Special Purpose Middleware: A Sensor Networks Case Study, Venkita Subramonian, Guoliang Xing, Christopher Gill, Ron Cytron
All Computer Science and Engineering Research
General purpose middleware has been shown to be effective in meeting diverse functional requirements for a wide range of distributed systems. Advanced middleware projects have also supported a single quality-of-service dimension such as real-time, fault tolerance, or small memory footprint. However, there is limited experience supporting multiple quality-of-service dimensions in mid-dleware to meet the needs of special purpose applications. Even though general purpose middleware can cover an entire spectrum of applications by supporting the union of all features required by each application, this approach breaks down for distributed real-time and embedded systems. In particular, features from one dimension such as …
Placing Servers For Session-Oriented Services, Sumi Choi, Yuval Shavitt
Placing Servers For Session-Oriented Services, Sumi Choi, Yuval Shavitt
All Computer Science and Engineering Research
The provisioning of dynamic forms of services is becoming the main stream of today's network. In this paper, we focus on services assisted by network servers and different forms of associated sessions. We identify two types of services: transparent, where the session is unaware of the server location, and configurable, where the sessions need to be configured to use their closest server. For both types we formalize the problem of optimally placing network servers and introduce approximated solutions. We present simulation result of approximations and heuristics. We also solve the location problem optimally for a special topology. We show, through …
The Fpx Kcpsm Module: An Embedded, Reconfigurable Active Processing Module For The Field Programmable Port Extender (Fpx), Henry Fu, John W. Lockwood
The Fpx Kcpsm Module: An Embedded, Reconfigurable Active Processing Module For The Field Programmable Port Extender (Fpx), Henry Fu, John W. Lockwood
All Computer Science and Engineering Research
While hardware plugins are well suited for processing data with high throughput, software plugins are well suited for implementing complex control functions. A plugin module has been implemented for the FPX that executes software on an embedded soft-core processor. By including this module in an FPX design, it is possible to implement active networking functions on the FPX using both hardware and software. The KCPSM, an 8-bit microcontroller developed by Xilinx Corp., has been embedded into an FPX module. The module includes circuits to be reprogrammed over the network and to execute new programs between the processing of data packerts. …
Fuzzycast: Media Broadcasting For Multiple Asynchronous Receivers, Marcel Waldvogel, Wei Deng, Ramaprabhu Janakiraman
Fuzzycast: Media Broadcasting For Multiple Asynchronous Receivers, Marcel Waldvogel, Wei Deng, Ramaprabhu Janakiraman
All Computer Science and Engineering Research
When using an on-demand media streaming system on top of a network with Multicast support, it is sometimes more efficient to use broadcast to distribute popular content. There has been a lot of research in broadcasting on-demand content to multiple, asynchronous receivers. In this paper, we propose a family of novel, practical techniques for broadcasting on-demand media, which achieve lowest known server/network bandwidth usage and I/O efficient client buffer management, while retaining the simplicity of a frame-based single channel scheme.
Fast Incremental Crc Updates For Ip Over Atm Networks, Florian Braun, Marcel Waldvogel
Fast Incremental Crc Updates For Ip Over Atm Networks, Florian Braun, Marcel Waldvogel
All Computer Science and Engineering Research
In response to the increasing network speeds, many operations in IP routers and similar devices are being made more efficient. With the advances in other areas of packet processing, the verification and regeneration of cyclic redundancy check (CRC) codes of the data link layer is likely to become a bottleneck in the near future. In this paper, we present a mechanism to defer CRC verification without compromising reliability. This opens the possibility of incremental updates of the CRC. We introduce a new high-speed technique and present efficient implementation, speeding up CRC processing by a factor of 15. Although the paper …
The Smart Port Card: An Embedded Unix Processor Architecture For Network Management And Active Networking, John D. Dehart, William D. Richard, Edward W. Spitznagel, David E. Taylor
The Smart Port Card: An Embedded Unix Processor Architecture For Network Management And Active Networking, John D. Dehart, William D. Richard, Edward W. Spitznagel, David E. Taylor
All Computer Science and Engineering Research
This paper describes the architecture of the Smart Port Card (SPC) designed for use with the Washington University Gigabit Switch. The SPC uses an embedded Intel Pentium processor running open-source NetBSD to support network management and active networking applications. The SPC physically connects between a switch port and a normal link adapter, allowing cell streams to be processed as they enter or leave the switch. In addition to the hardware architecture, this paper describes current and future applications for the SPC.
Evaluation Of Motion-Jpeg2000 For Video Processing, Wei Yu, Ruibiao Qiu, Jason Fritts
Evaluation Of Motion-Jpeg2000 For Video Processing, Wei Yu, Ruibiao Qiu, Jason Fritts
All Computer Science and Engineering Research
The new ISO/ITU-T standard for still image coding, JPEG2000, has been shown to provide superior coding efficiency to the previous standard, JPEG. Because of the superb performance of JPEG2000, it is reasonable to argue that Motion-JPEG2000, the corresponding moving picture coding standard of JPEG2000, has equally outstanding performance. However, there has not been a sufficient performance evaluation of Motion-JPEG2000. To this end, we have studied the potential of Motion-JPEG2000 for video processing. Our experiments show that Motion-JPEG2000 provides high compression performance, strong error resilience, and good perceptual image quality. Together with a rich set of features inherited from JPEG2000, Motion-JPEG2000 …
Performance Of Deferred Reservations In Data Networks, Samphel Norden, Jonathan Turner
Performance Of Deferred Reservations In Data Networks, Samphel Norden, Jonathan Turner
All Computer Science and Engineering Research
This paper studies the performance of deferred resource reservation in data networks. Conventional resource reservation protocols, such as PNNI and RSVP adopt an all-or-nothing approach, where partially acquired resources must be released if resources are not available at all links on the chosen path. During periods of high network load, this leads users to retry requests repeatedly, adding control traffic at exactly the time when the network's capacity to process that control traffic is exhausted. Deferred REServation (DRES) can significantly improve performance by reducing the overall call rejection probability, allowing more traffic to be carried, using the same resources. Call …
An Efficient Quality Scalable Motion-Jpeg2000 Transmission Scheme, Ruibiao Qiu, Wei Yu
An Efficient Quality Scalable Motion-Jpeg2000 Transmission Scheme, Ruibiao Qiu, Wei Yu
All Computer Science and Engineering Research
Video application over the Internet are getting increasingly popular because of the explosive growth of the Internet. However, video packets loss due to network congestions can degrade the video quality substantially. In this paper, we propose a transmission scheme for Motion-JPEG2000. It can be implemented in an active network environment efficiently. Our simulation shows that our scheme gracefully adapts to network congestion and improves the quality of video transmission in congested IP networks.
Embedding Images In Non-Flat Spaces, Robert Pless
Embedding Images In Non-Flat Spaces, Robert Pless
All Computer Science and Engineering Research
Multi-dimensional scaling is an analysis tool which transforms pairwise distances between points to an embedding of points in space which are consistent with those distances. Two recent techniques in statistical patter recognition, locally linear embedding (LLE) and Isomap, give a mechanism for finding the structure underlying point sets for which comparisons or distances are only meaningful between nearby points. We give a direct method to extend the embedding algorithm to new topologies, finding the optimal embedding of points whose geodesic distance on a surface mathes the given pairwise distance measurements. Surfaces considered include spheres, cylinders, tori, and their higher dimensional …
A Termination Detection Protocol For Use In Mobile Ad Hoc Networks, Gruia-Catalin Roman, Jamie Payton
A Termination Detection Protocol For Use In Mobile Ad Hoc Networks, Gruia-Catalin Roman, Jamie Payton
All Computer Science and Engineering Research
As computing devices become smaller and wireless networking technologies improve, the popularity of mobile computing continues to rise. In today's business world, many consider devices such as cell phones, PDAs, and laptops as essential tools. As these and other devices become increasingly independent of the wired infrastructure, new kinds of applications that assume an ad hoc network infrastructure will need to be deployed. Such a setting poses new challenges for the software developer, e.g., the lack of an established network topology, bandwidth limitations, and frequent disconnections. In this paper, we begin to explore design strategies for developing applications over ad …
Parbit: A Tool To Transform Bitfiles To Implement Partial Reconfiguration Of Field Programmable Gate Arrays (Fpgas), Edson L. Horta, John W. Lockwood
Parbit: A Tool To Transform Bitfiles To Implement Partial Reconfiguration Of Field Programmable Gate Arrays (Fpgas), Edson L. Horta, John W. Lockwood
All Computer Science and Engineering Research
Field Programmable Gate Arrays (FPGAs) can be partially reconfigured to implement Dynamically loadable Hardware Plugin (DHP) modules. A tool called PARBIT has been developed that transforms FPGA configuration bitfiles to enable DHP modules. With this tool it is possible to define a partial reconfigurable area inside the FPGA and download it into a specified region of the FPGA device. One or more DHPs, with different sizes can be implemented using PARBIT.
Relying On Safe Distance To Ensure Consistent Group Membership In Ad Hoc Networks, Qingfeng Huang, Christine Julien, Gruia-Catalin Roman, Ali Hazemi
Relying On Safe Distance To Ensure Consistent Group Membership In Ad Hoc Networks, Qingfeng Huang, Christine Julien, Gruia-Catalin Roman, Ali Hazemi
All Computer Science and Engineering Research
The design of ad hoc mobile applications often requires the availability of a consistent view of the application state among the participating hosts. Such views are important because they simplify both the programming and verification tasks. Essential to constructing a consitent view is the ability to know what hosts are within proximity of each other, i.e., form a group in support of the particular application. In this paper we propose a protocol that allows hosts within communication range to maintain a consistent view of the group membership despite movement and frequent disconnections. The novel features of this protocol are its …
Scheduling Processing Resources In Programmable Routers, Prashanth Pappu, Tilman Wolf
Scheduling Processing Resources In Programmable Routers, Prashanth Pappu, Tilman Wolf
All Computer Science and Engineering Research
To provide flexibility in deploying new protocols and services, general-purpose processing engines are being placed in the datapath of routers. Such network processors are typically simple RISC multiprocessors that perform forwarding and custom application processing of packets. The inherent unpredictability of execution time of arbitrary instruction code poses a significant challenge in providing QoS guarantees for data flows that compete for such processing resources in the network. However, we show that network processing workloads are highly regular and predictable. Using estimates of execution times of various applications on packets of given lengths, we provide a method for admission control and …
Design Of Wavelength Converting Switches For Optical Burst Switching, Jeyashankher Ramamirtham, Jonathan Turner
Design Of Wavelength Converting Switches For Optical Burst Switching, Jeyashankher Ramamirtham, Jonathan Turner
All Computer Science and Engineering Research
Optical Burst Switching (OBS) is an experimental network technology that enables the construction of very high capacity routers, using optical data paths and electronic control. In this paper, we study two designs for wavelength converting switches that are suitable for use in optical burst switching systems and evaluate their performance. Both designs use tunable lasers to implement wavelength conversion. One is strictly nonblocking design, that also requires optical crossbars. The second substitutes Wavelength Grating Routers (WGR) for the optical crossbars, reducing cost, but introducing some potential for blocking. We show how the routing problem for the WGR-based switches can be …
Local Search And Encoding Schemes For Soft Constraint Minimization Problems, Michael P. Moran, Weixiong Zhang
Local Search And Encoding Schemes For Soft Constraint Minimization Problems, Michael P. Moran, Weixiong Zhang
All Computer Science and Engineering Research
Soft constraint minimization problems (SCMPs) contain hard constraints that cannot be violated and soft constraints that may be violated but carry penalties if not satisfied. In this paper, we first extend local search, WalkSAT in particular, to SCMPs and study the existing SAT encoding schemes for SCMPs. We propose a general encoding method called k-encoding. We then investigate the effects of local search neiborhood structures introduced by encoding schemes and analyze the anytime performance of extended WalkSAT using different encoding methods. Our experimental results on various graph coloring problems show that a direct extension of WalkSAT is most effective, and …
Aggregated Hierarchical Multicast For Active Networks, Tilman Wolf, Sumi Y. Choi
Aggregated Hierarchical Multicast For Active Networks, Tilman Wolf, Sumi Y. Choi
All Computer Science and Engineering Research
Active Networking is the basis for a range of new and innovative applications that make use of computational resources inside network routers. One such application is Aggregated Hierarchical Multicast, which aims at implementing efficient many-to-many communication. In certain scenarios it is possible to transmit less accurate, aggregated data and thus achieve better scalability. Using Active Networks, this aggregation computation can be done transparently by network routers without end system support. We present how aggregated data streams can be structured in a hierarchical fashion to allow easy access of data at the desired aggregation level. We introduce two application examples to …
A Distributed Annotation System, Robin Dowell
A Distributed Annotation System, Robin Dowell
All Computer Science and Engineering Research
One goal of any genome project is the elucidation of hte primary sequence of DNA contained within a given species. While the availability ot the primary sequence itself is valuable, it does not reach its full potential until i has been annotated. Generally defined, annotation is descriptive information or commentary added to text, in this case genomic sequence. Without a mechanism for collecting, recording, and disseminating community-based annotation, a valuable source of information is severely diminshed. In this report I outline the design and implementation of a Distributed Annotation System (DAS). DAS allowes sequence annotations to be decentralized among multiple …
Phase Transitions And Backbones Of Constraint Minimization Problems, Weixiong Zhang
Phase Transitions And Backbones Of Constraint Minimization Problems, Weixiong Zhang
All Computer Science and Engineering Research
Many real-world problems involve constraints that cannot be all satisfied. The goal toward an overconstrained problem is to find solutions minimizing the total number of constraints violated. We call such a problem constraint minimization problem (CMP). We study the behavior of the phase transitions and backbones of CMP. We first investigate the relationship between the phase transitions of Boolean satisfiability, or precisely 3-SAT (a well-studied NP-complete decision problem), and the phase transitions of MAX 3-SAT (an NP-hard optimization problem). To bridge the gap between the easy-hard-easy phase transitions of 3-SAT, in which solutions of bounded quality, e.g., solutions with at …
A Proposal For A Scalable Internet Multicast Architecture, Sherlia Shi
A Proposal For A Scalable Internet Multicast Architecture, Sherlia Shi
All Computer Science and Engineering Research
We propose a new network and system architecture for multicast in the Internet. Our main objectives are to find a cost-effective way to scale to a large number of multicast groups whose members are geographically dispersed, and to enable small and less capable devices to participate in group communications. In order to preserve the efficiency of data distribution gained by multicast, while avoiding the control complexity previously exhibited by IP multicast, we propose the use of an overlay network for multicast services. We construct "virtual" multicast trees, which consist of unicast connections joining multicast servers in the network. These servers …
Indra: A Distributed Approach To Network Intrusion Detection And Prevention, Qi Zhang, Ramaprabhu Janakiraman
Indra: A Distributed Approach To Network Intrusion Detection And Prevention, Qi Zhang, Ramaprabhu Janakiraman
All Computer Science and Engineering Research
While advances in computer and communications technology have made the network ubiquitous, they ahve also rendered networked systems vulnerable to malicious attacks orchestrated from a distance. These attacks, usually called cracker attacks or intrusions, start with crackers infiltrating a network through a vulnerable host and then going on to launch further attacks. Crackers depend on increasingly sophisticated techniques like using distributed attack sources. On the other hand, software that guards against them remains rooted in traditional centralized techniques, presenting an easily-targetable single point of failure. Scalable, distributed network intrusion prevention software is sorely needed. We propose Indra - a distributed …
Formal Specification And Design Of Mobile Systems, Gruia-Catalin Roman, Christine Julien, Qingfeng Huang
Formal Specification And Design Of Mobile Systems, Gruia-Catalin Roman, Christine Julien, Qingfeng Huang
All Computer Science and Engineering Research
Termination detection, a classical problem in distributed computing, is revisited in the new setting provided by the emerging mobile computing technology. A simple solution tailored for use in ad hoc networks is employed as a vehicle for demonstrating the applicability of formal requirements and design strategies to the new field of mobile computing. The approach is based on well understood techniquest in specification refinement, but the methodology is tailored to mobile applications and helps designers address novel concerns such as the mobility of hosts, transient interactions, and specific coordination constructs. The proof logic and programming notation of Mobile UNITY provide …