The PROSPER toolkit

The PROSPER (Proof and Specification Assisted Design Environments) project advocates the use of toolkits which allow existing verification tools to be adapted to a more flexible format so that they can be treated as components. A system incorporating such tools becomes another component that can be embedded in an application. This paper describes the software toolkit developed by the project. The nature of communication between components is specified in a language-independent way. It is implemented in several common programming languages to allow a wide variety of tools to have access to the toolkit. Published online: 19 November 2002 Work funded by ESPRIT Framework IV Grant LTR 26241. RID="*" ID="*"Michael Norrish is supported by the Michael and Morven Heller Research Fellowship at St. Catharine’s College, Cambridge. RID="**" ID="**"Konrad Slind is now at the School of Computing, University of Utah, Salt Lake City UT 84112, USA.     

Underflow revisited

Underflow is a floating-point phenomenon. Although the use of gradual underflow as defended in [2] and [3] is now widespread, most numerical analysts may not be aware of the fact that several implementations of the same principle are in existence, leading to different behavior of code on different platforms, mainly with respect to exception signaling. We intend to thoroughly discuss the slight differences among these implementations. Examples will be taken from current hardware and from our own multiprecision software class library. Throughout the discussion the focus is on the analysis of the phenomenon and not on any implementation issues. Many programmers are also unaware of the fact that the IEEE 754 and 854 standards do not guarantee that a program will deliver identical results on all conforming systems. Of all the differences that can occur cross-platform, the underflow exception is just one. Received: January 2002 / Accepted: June 2002 RID="*" ID="*"Research Director, FWO-Vlaanderen RID="**" ID="**"Supported by an NOI-grant from the Universiteit Antwerpen (UIA) RID="***" ID="***"Postdoctoral Fellow, FWO-Vlaanderen RID="****" ID="****"Research Fellow, IWT (Institute for Science and Technology)     

Protocol synthesis and re-synthesis with optimal allocation of resources based on extended Petri nets

Protocol synthesis is used to derive a protocol specification, that is, the specification of a set of application components running in a distributed system of networked computers, from a specification of services (called the service specification) to be provided by the distributed application to its users. Protocol synthesis reduces design costs and errors by specifying the message exchanges between the application components, as defined by the protocol specification. In general, maintaining such a distributed application involves applying frequent minor modifications to the service specification due to changes in the user requirements. Deriving the protocol specification after each modification using the existing synthesis methods is considered expensive and time consuming. Moreover, we cannot identify what changes we should make to the protocol specification in correspondence to the changes in the service specification. In this paper, we present a new synthesis method to re-synthesize only those parts of the protocol specification that must be modified in order to satisfy the changes in the service specification. The method consists of a set of simple rules that are applied to the protocol specification written in an extended Petri net model. An application example is given along with some experimental results. Received: July 2001 / Accepted: July 2002 RID="*" ID="*" Supported by International Communications Foundation (ICF), Japan RID="**" ID="**" Supported by Communications and Information Technology Ontario (CITO) and Natural Sciences and Engineering Research Council (NSERC), Canada RID="*" ID="*" Supported by International Communications Foundation (ICF), Japan     

Restoration by path concatenation: fast recovery of MPLS paths

A new general theory about restoration of network paths is first introduced. The theory pertains to restoration of shortest paths in a network following failure, e.g., we prove that a shortest path in a network after removing k edges is the concatenation of at most k+1 shortest paths in the original network. The theory is then combined with efficient path concatenation techniques in MPLS (multi-protocol label switching), to achieve powerful schemes for restoration in MPLS based networks. We thus transform MPLS into a flexible and robust method for forwarding packets in a network. Finally, the different schemes suggested are evaluated experimentally on three large networks (a large ISP, the AS graph of the Internet, and the full Internet topology). These experiments demonstrate that the restoration schemes perform well in actual topologies. Received: December 2001 / Accepted: July 2002 RID="*" ID="*" This research was supported by a grant from the Ministry of Science, Israel     

A reconfigurable architecture for autonomous visual-navigation

Abstract. This paper describes the design of a reconfigurable architecture for implementing image processing algorithms. This architecture is a pipeline of small identical processing elements that contain a programmable logic device (FPGA) and double port memories. This processing system has been adapted to accelerate the computation of differential algorithms. The log-polar vision selectively reduces the amount of data to be processed and simplifies several vision algorithms, making possible their implementation using few hardware resources. The reconfigurable architecture design has been devoted to implementation, and has been employed in an autonomous platform, which has power consumption, size and weight restrictions. Two different vision algorithms have been implemented in the reconfigurable pipeline, for which some experimental results are shown. Received: 30 March 2001 / Accepted: 11 February 2002 RID="*" ID="*" This work has been supported by the Ministerio de Ciencia y Tecnología and FEDER under project TIC2001-3546 Correspondence to: J.A. Boluda     

An improved lower bound for the time complexity of mutual exclusion

We establish a lower bound of remote memory references for N-process mutual exclusion algorithms based on reads, writes, or comparison primitives such as test-and-set and compare-and-swap. Our bound improves an earlier lower bound of established by Cypher. Our lower bound is of importance for two reasons. First, it almost matches the time complexity of the best known algorithms based on reads, writes, or comparison primitives. Second, our lower bound suggests that it is likely that, from an asymptotic standpoint, comparison primitives are no better than reads and writes when implementing local-spin mutual exclusion algorithms. Thus, comparison primitives may not be the best choice to provide in hardware if one is interested in scalable synchronization. Received: January 2002 / Accepted: September 2002 RID="*" ID="*" Work supported by NSF grants CCR 9732916, CCR 9972211, CCR 9988327, ITR 0082866, and CCR 0208289.     

Gain-scheduled H ∞ filtering of parameter-varying discrete-time systems via parameter-dependent Lyapunov functions

This paper is concerned with the problem of gain-scheduled H _∞ filter design for a class of parameter-varying discrete-time systems. A new LMI-based design approach is proposed by using parameter-dependent Lyapunov functions. Recommended by Editorial Board member Huanshui Zhang under the direction of Editor Jae Weon Choi. This work was supported in part by the National Natural Science Foundation of P. R. China under Grants 60874058, by 973 program No 2009CB320600, but also the National Natural Science Foundation of Province of Zhejiang under Grants Y107056, and in part by a Research Grant from the Australian Research Council. Shaosheng Zhou received the B.S. degree in Applied Mathematics and the M.Sc. and Ph.D. degrees in Electrical Engineering, in January 1992, July 1996 and October 2001, from Qufu Normal University and Southeast University. His research interests include nonlinear control and stochastic systems. Baoyong Zhang received the B.S. and M.Sc. degrees in Applied Mathematics, in July 2003 and July 2006, all from Qufu Normal University. His research interests include and nonlinear systems, robust control and filtering. Wei Xing Zheng received the B.Sc. degree in Applied Mathematics and the M.Sc. and Ph.D. degrees in Electrical Engineering, in January 1982, July 1984 and February 1989, respectively, all from the Southeast University, Nanjing, China. His research interests include signal processing and system identification.     

An Approach to Security Requirements Engineering for a High Assurance System*

Requirements specifications for high-assurance secure systems are rare in the open literature. This paper examines the development of a requirements document for a multilevel secure system that must meet stringent assurance and evaluation requirements. The system is designed to be secure, yet combines popular commercial components with specialised high-assurance ones. Functional and non-functional requirements pertinent to security are discussed. A multidimensional threat model is presented. The threat model accounts for the developmental and operational phases of system evolution and for each phase accounts for both physical and non-physical threats. We describe our team-based method for developing a requirements document and relate that process to techniques in requirements engineering. The system requirements document presented provides a calibration point for future security requirements engineering techniques intended to meet both functional and assurance goals. RID="*" ID="*"The views expressed in this paper are those of the authors and should not be construed to reflect those of their employers or the Department of Defense. This work was supported in part by the MSHN project of the DARPA/ITO Quorum programme and by the MYSEA project of the DARPA/ATO CHATS programme. Correspondence and offprint requests to: T. Levin, Department of Computer Science, Naval Postgraduate School, Monterey, CA 93943-5118, USA. Tel.: +1 831 656 2339; Fax: +1 831 656 2814; Email: levin@nps.navy.mil     

An efficient distributed algorithm for constructing small dominating sets

The dominating set problem asks for a small subset D of nodes in a graph such that every node is either in D or adjacent to a node in D. This problem arises in a number of distributed network applications, where it is important to locate a small number of centers in the network such that every node is nearby at least one center. Finding a dominating set of minimum size is NP-complete, and the best known approximation is logarithmic in the maximum degree of the graph and is provided by the same simple greedy approach that gives the well-known logarithmic approximation result for the closely related set cover problem. We describe and analyze new randomized distributed algorithms for the dominating set problem that run in polylogarithmic time, independent of the diameter of the network, and that return a dominating set of size within a logarithmic factor from optimal, with high probability. In particular, our best algorithm runs in rounds with high probability, where n is the number of nodes, is one plus the maximum degree of any node, and each round involves a constant number of message exchanges among any two neighbors; the size of the dominating set obtained is within of the optimal in expectation and within of the optimal with high probability. We also describe generalizations to the weighted case and the case of multiple covering requirements. Received: January 2002 / Accepted: August 2002 RID="*" ID="*" Supported by NSF CAREER award NSF CCR-9983901 RID="*" ID="*" Supported by NSF CAREER award NSF CCR-9983901     

Model-checking multi-threaded distributed Java programs

State-space exploration is a powerful technique for verification of concurrent software systems. Applying it to software systems written in standard programming languages requires powerful abstractions (of data) and reductions (of atomicity), which focus on simplifying the data and control, respectively, by aggregation. We propose a reduction that exploits a common pattern of synchronization, namely, the use of locks to protect shared data structures. This pattern of synchronization is particularly common in concurrent Java programs, because Java provides built-in locks. We describe the design of a new tool for state-less state-space exploration of Java programs that incorporates this reduction. We also describe an implementation of the reduction in Java PathFinder, a more traditional state-space exploration tool for Java programs. Published online: 2 October 2002 RID="*" ID="*"Present address: Computer Science Dept., SUNY at Stony Brook, Stony Brook, NY 11794-4400, USA. The author gratefully acknowledges the support of ONR under Grants N00014-99-1-0358 and N00014-01-1-0109 and the support of NSF under Grant CCR-9876058.     

Troubleshooting: NP-hardness and solution methods

 Troubleshooting is one of the areas where Bayesian networks are successfully applied [9]. In this paper we show that the generally defined troubleshooting task is NP-hard. We propose a heuristic function that exploits the conditional independence of all actions and questions given the fault of the device. It can be used as a lower bound of the expected cost of repair in heuristic algorithms searching an optimal troubleshooting strategy. In the paper we describe two such algorithms: the depth first search algorithm with pruning and the AO^* algorithm. RID="*" ID="*" The authors were supported through grant #87.2 of National Centre for IT Research, Denmark and through grant MSMT VS96008 from the Ministry of Education, Youth and Sports of the Czech Republic. We would like to thank Finn Verner Jensen for inspiring us to work on the discussed problem and for many valuable comments on this paper. We are grateful to Claus Skaanning for the detailed explanation of the BATS troubleshooter approach and to anonymous reviewers for helpful suggestions.     

Local tests for consistency of support hyperplane data

Support functions and samples of convex bodies in R ⁿ are studied with regard to conditions for their validity or consistency. Necessary and sufficient conditions for a function to be a support function are reviewed in a general setting. An apparently little known classical such result for the planar case due to Rademacher and based on a determinantal inequality is presented and a generalization to arbitrary dimensions is developed. These conditions are global in the sense that they involve values of the support function at widely separated points. The corresponding discrete problem of determining the validity of a set of samples of a support function is treated. Conditions similar to the continuous inequality results are given for the consistency of a set of discrete support observations. These conditions are in terms of a series of local inequality tests involving only neighboring support samples. Our results serve to generalize existing planar conditions to arbitrary dimensions by providing a generalization of the notion of nearest neighbor for plane vectors which utilizes a simple positive cone condition on the respective support sample normals.This work partially supported by the Center for Intelligent Control Systems under the U.S. Army Research Office Grant DAAL03-92-G-0115, the Office of Naval Research under Grant N00014-91-J-1004, and the National Science Foundation under Grant MIP-9015281.Partially supported by the National Science Foundation under grant IRI-9209577 and by the U.S. Army Research Office under grant DAAL03-92-G-0320     

Algorithms for bichromatic line-segment problems and polyhedral terrains

We consider a variety of problems on the interaction between two sets of line segments in two and three dimensions. These problems range from counting the number of intersecting pairs between m blue segments andn red segments in the plane (assuming that two line segments are disjoint if they have the same color) to finding the smallest vertical distance between two nonintersecting polyhedral terrains in three-dimensional space. We solve these problems efficiently by using a variant of the segment tree. For the three-dimensional problems we also apply a variety of recent combinatorial and algorithmic techniques involving arrangements of lines in three-dimensional space, as developed in a companion paper.Work on this paper by the first author has been supported in part by the National Science Foundation under Grant CCR-9002352. Work by the second author was supported in part by the National Science Foundation under Grant CCR-8714565. The fourth author has been supported in part by the Office of Naval Research under Grant N0014-87-K-0129, by the National Science Foundation under Grant NSF-DCR-83-20085, by grants from the Digital Equipment Corporation and the IBM Corporation, and by a grant from the US-Israeli Binational Science Foundation.     

Delay-dependent robust H ∞ control for uncertain fuzzy Markovian jump systems

This paper is concerned with the problem of delay-dependent robust H _∞ control for uncertain fuzzy Markovian jump systems with time delays. The purpose is to design a mode-dependent state-feedback fuzzy controller such that the closed-loop system is robustly stochastically stable and satisfies an H _∞ performance level. By introducing slack matrix variables, a delay-dependent sufficient condition for the solvability of the problem is proposed in terms of linear matrix inequalities. An illustrative example is finally given to show the applicability and effectiveness of the proposed method. Recommended by Editorial Board member Young Soo Suh under the direction of Editor Jae Weon Choi. This work is supported by the National Science Foundation for Distinguished Young Scholars of P. R. China under Grant 60625303, the Specialized Research Fund for the Doctoral Program of Higher Education under Grant 20060288021, and the Natural Science Foundation of Jiangsu Province under Grant BK2008047. Yashun Zhang received the B.S. and M.S. degrees in Control Science and Control Engineering from Hefei University of Science and Technology in 2003 and 2006. He is currently a Ph.D. student in Control Science and Control Engineering, Nanjing University of Science and Technology. His research interests include fuzzy control, sliding mode control and nonlinear control. Shengyuan Xu received the Ph.D. degree in Control Science and Control Engineering from Nanjing University of Science and Technology in 1999. His research interests include robust filtering and control, singular systems, time-delay systems and nonlinear systems. Jihui Zhang is a Professor in the School of Automation Engineering of Qingdao University, China. His main areas of interest are discrete event dynamic systems, production planning and control, and operations research.     

Tolerating malicious gossip

A new class of gossip protocols to diffuse updates securely is presented. The protocols rely on annotating updates with the path along which they travel. To avoid a combinatorial explosion in the number of annotated updates, rules are employed to choose which updates to keep. Different sets of rules lead to different protocols. Results of simulated executions for a collection of such protocols are described – the protocols would appear to be practical, even in large networks. Received: October 2001 / Accepted: July 2002 Supported in part by ARPA/RADC grant F30602-96-1-0317, AFOSR grant F49620-00-1-0198, Defense Advanced Research Projects Agency (DARPA) and Air Force Research Laboratory Air Force Material Command USAF under agreement number F30602-99-1-0533, National Science Foundation Grant 9703470, and a grant from Intel Corporation. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of these organizations or the U.S. Government.     

Tight bounds for shared memory systems accessed by Byzantine processes

We provide efficient constructions and tight bounds for shared memory systems accessed by n processes, up to t of which may exhibit Byzantine failures, in a model previously explored by Malkhi et al. [21]. We show that sticky bits are universal in the Byzantine failure model for n ≥ 3t + 1, an improvement over the previous result requiring n ≥ (2t + 1)(t + 1). Our result follows from a new strong consensus construction that uses sticky bits and tolerates t Byzantine failures among n processes for any n ≥ 3t + 1, the best possible bound on n for strong consensus. We also present tight bounds on the efficiency of implementations of strong consensus objects from sticky bits and similar primitive objects. Research supported in part by a grant from the Israel Science Foundation, and by the Hermann Minkowski Minerva Center for Geometry at Tel Aviv University. This work was partially completed while at AT&T Labs and while visiting the Institute for Advanced Study, Princeton, NJ. Research supported in part by US-Israel Binational Science Foundation Grant 2002246. This work was partially completed while visiting AT&T Labs. This work was partially completed while at AT&T Labs. Research supported in part by the National Science Foundation under Grant No. CCR-0331584. A preliminary version of the results presented in this paper appeared in [23].     

When is a controllerH ∞-optimal?

This paper examines conditions under which a given single input, single output, linear time invariant control system isH ^∞-optimal with respect to weighted combinations of its sensitivity function and its complementary sensitivity function. The specific weighting functions considered are defined in terms of the given plant and nominal controller. This paper shows that a large class of practical controllers areH ^∞-optimal, including typical stable controllers. This research was supported in part by the National Science Foundation under Grant No. ECS-8451519, grants from Honeywell, 3M, Sperry, and E. F. Johnson Company, ONR Research Grant N00014-82-C-0157, and AFOSR Research Grant F49620-86-C-0001.     

Robustness of Nonlinear Delay Equations with Respect to Input Perturbations: a Trajectory-Based Approach

 The effect of input perturbations on the stability properties of nonlinear time-varying delay differential equations is studied from a trajectory-based point of view. Thereby the semi-global stability results from [MSR2], where a Lyapunov approach is taken, are broadened to a much larger class of delay differential equations. Applications to the stabilization of partially linear cascade systems with delay using partial state feedback are briefly outlined. Date received: January 9, 2001. Date revised: April 15, 2002. RID="*" ID="*"This paper presents research results of the Belgian programme on Interuniversity Poles of Attraction, initiated by the Belgian State, Prime Minister's Office for Science, Technology and Culture (IUAP P4/02). The scientific responsibility rests with its authors. Luc Moreau is a Postdoctoral Fellow of the Fund for Scientific Research—Flanders (Belgium) (F.W.O.-Vlaanderen) and a recipient of an Honorary Fellowship of the Belgian American Educational Foundation. Part of this work was done while Luc Moreau was supported by a BOF grant of the Ghent University.     

Optimal parallel verification of minimum spanning trees in logarithmic time

We present the first optimal parallel algorithms for the verification and sensitivity analysis of minimum spanning trees. Our algorithms are deterministic and run inO(logn) time and require linear-work in the CREW PRAM model. These algorithms are used as a subroutine in the linear-work randomized algorithm for finding minimum spanning trees of Cole, Klein, and Tarjan. Research partially supported by a National Science Foundation Graduate Fellowship and by DIMACS (Center for Discrete Mathematics and Theoretical Computer Science), a National Science Foundation Science and Technology Center, Grant No. NSF-STC88-09648. Research at Princeton University was partially supported by the National Science Foundation, Grant No. CCR-8920505, the Office of Naval Research, Contract No. N00014-91-J-1463, and by DIMACS (Center for Discrete Mathematics and Theoretical Computer Science), a National Science Foundation Science and Technology Center, Grant No. NSF-STC88-09648.