Time-dependent distributed systems: proving safety,liveness and real-time properties

Most communication protocol systems utilize timers to implement real-time constraints between event occurrences. Such systems are said to betime-dependent if the real-time constraints are crucial to their correct operation. We present a model for specifying and verifying time-dependent distributed systems. We consider networks of processes that communicate with one another by message-passing. Each process has a set of state variables and a set of events. An event is described by a predicate that relates the values of the network's state variables immediately before to their values immediately after the event occurrence. The predicate embodies specifications of both the event's enabling condition and action. Inference rules for both safety and liveness properties are presented. Real-time progress properties can be verified as safety properties. We illustrate with three sliding window data transfer protocols that use modulo-2 sequence numbers. The first protocol operates over channels that only lose messages. It is a time-independent protocol. The second and third protocols operate over channels that lose, reorder, and duplicate messages. For their correct operation, it is necessary that messages in the channels have bounded lifetimes. They are time-dependent protocols.A. Udaya Shankar received the B. Tech. degree in Electrical Engineering from the Indian Institute of Technology, Kanpur, in 1976, the M.S. degree in Computer Engineering from Syracuse University, Syracuse, NY, in 1978, and the Ph.D. degree in Electrical Engineering from the University of Texas at Austin, in 1982. Since January 1983, he has been an Assistant Professor in the Department of Computer Science, University of Maryland, College Park. Since September 1985, he has been in the Institute for Advanced Computer Studies at the University of Maryland. His current research interests include modeling and verification of distributed systems, communication protocols, and real-time systems. He is a member of IEEE and ACM.Simon S. Lam is a Professor of Computer Sciences at the University of Texas at Austin and holds the Second David Bruton Jr. Centennial Professorship. His research interests are in the areas of computer networks, communication protocols, performance modeling, and the specification and verification of distributed systems. He serves on the editorial boards of three journals, IEEE Transactions on Communications, Performance Evaluation, and Proceedings of IEEE, and he is an IEEE Fellow. He received the BSEE degree (with Distinction) from Washington State University in 1969, and the MS and Ph.D. degrees from UCLA in 1970 and 1974 respectively. Prior to joining the University of Texas faculty, he was with the IBM T.J. Watson Research center from 1974 to 1977.Work supported by National Science Foundation under Grant No. ECS 85-02113Work supported by National Science Foundation under Grant No. ECS 83-04734     

Self-stabilization over unreliable communication media

Summary A self-stabilizing system has the property that it will converge to a desirable state when started from any state. Most previous researchers assumed that processes in self-stabilizing systems may communicate through shared variables while those that studied meassage passing systems allowed messages with unbounded size. This paper discusses the development of self-stabilizing systems which communicate through message passing, and in which messages may be lost in transit. The systems presented all use fixed size message headers. First, a selfstabilizing version of theAlternating Bit Protocol, a fundamental communication protocol for transmitting data across an unreliable communication medium, is presented. Secondly, the alternating-bit protocol is used to construct a self-stabilizing token ring. Yehuda Afek received a B.Sc. in Electrical Engineering from the Technion and an M.S. and Ph.D. in Computer Science from the University of California, Los Angeles. In 1985 he joined the Distributed Systems research Department in AT&T Bell Laboratories and in 1988 he joined the Department of Computer Science in Tel-Aviv University. His interests include communication protocols, distributed systems, and asynchronous shared memories. Geoffrey M. Brown received the BS degree in Engineering from Swarthmore College in 1982, the MS degree in Electrical Engineering from Stanford University in 1983, and the Ph.D. degree in Electrical Engineering from the University of Texas at Austin in 1987. From 1983 to 1984 he worked for Motorola in Austin, TX. Currently he is an Assistant Professor in the School of Electrical Engineering at Cornell University. In 1990, Brown was named a Presidential Young Investigator by the National Science Foundation.This work supported in part by NSF grant CCR-9058180     

Self-stabilization of dynamic systems assuming only read/write atomicity

Summary Three self-stabilizing protocols for distributed systems in the shared memory model are presented. The first protocol is a mutual-exclusion prootocol for tree structured systems. The second protocol is a spanning tree protocol for systems with any connected communication graph. The thrid protocol is obtianed by use offair protoco combination, a simple technique which enables the combination of two self-stabilizing dynamic protocols. The result protocol is a self-stabilizing, mutualexclusion protocol for dynamic systems with a general (connected) communication graph. The presented protocols improve upon previous protocols in two ways: First, it is assumed that the only atomic operations are either read or write to the shared memory. Second, our protocols work for any connected network and even for dynamic network, in which the topology of the network may change during the excution. Shlomi Dolev received his B.Sc. in Civil Engineering and B.A. in Computer Science in 1984 and 1985, and his M.Sc. and Ph.D. in computer Sciene in 1989 and 1992 from the Technion Israel Institute of Technology. He is currently a post-dotoral fellow in the Department of Computer Science at Texas A & M Univeristy. His current research interests include the theoretical aspects of distributed computing and communcation networks. Amos Israeli received his B.Sc. in Mathematics and Physics from Hebrew University in 1976, and his M.Sc. and D.Sc. in Computer Science from the Weizmann Institute in 1980 and the Technion in 1985, respectively. Currently he is a sensior lecturer at the Electrical Engineering Department at the Technion. Prior tot his he was a postdoctoral fellow at the Aiken Computation Laboratory at harvard. His research interests are in Parellel and Distributed Computing and in Robotics. In particular he has worked on the design and analysis of Wait-Free and Self-Stabilizing distributed protocols. Shlomo Moran received his B.Sc. and D.Sc. degrees in matheamtics from Technion, Israel Institute of Technology, Haifa, in 1975 and 1979, respectively. From 1979 to 1981 he was assistant professors and a visiting research specialist at the University of Minnesota, Minneapolis. From 1981 to 1985 he was a senior lecturer at the Department of Computer Science. Technion, and from 1985 to 1986 he visted at IBM Thoas J. Watson Research Center, Yorktown Heights. From 1986 to 1993 he was an associated professor at the Department of Computer Science, Technin. in 1992–3 he visited at AT & T Bell Labs at Murray Hill and at Centrum voor Wiskunde en Informatica, Amsterdam. From 1993 he is a full professor at the Department of Computer Science, Technion. His researchinterests include distributed algorithm, computational complexity, combinatorics and grapth theory.Part of this research was supported in part by Technion V.P.R. Funds — Wellner Research Fund, and by the Foundation for Research in Electronics, Computers and Communictions, administrated by the Israel Academy of Sciences and Humanities.     

Specification and analysis of a data transfer protocol using systems of communicating machines

Summary A model for communication protocols calledsystems of communicating machines is used to specify a data transfer protocol with variable window size (e.g., HDLC), which is an arbitrary nonnegative integer, and to analyze it for freedom from deadlocks. The model uses a combination of finite state machines and variables. This allows the size of the specification (i.e., number of states and variables) to be linear in the window size, a considerable reduction from the pure finite state machine model. A new type of analysis is demonstrated which we callsystem state analysis. This is similar to thereachability analysis used in the pure finite state model, but it provides substantial simplication by reducing the number of states generated. For example, with the protocol in this paper, ifw is the window size, then the global analysis producesO(w ⁵) states, while the system state analysis producesO(w ³) states. The system state analysis is then combined with an inductive proof, extending the analysis to all nonnegative integersw. Gilbert M. Lundy, Jr was born in New Orleans, Louisiana, in 1954. After completing schools in Plano, Texas, he attended Texas A & M University, receiving the B.A. in mathematics (1976). From 1977–81 he served as a Lieutenant in the U.S. Army, based at Fort Ord, California. From 1981–84 he was a software engineer at E-Systems, in Dallas, Texas. During this period he also completed the M.S. program in Computer Science at the University of Texas at Dallas. From 1984 to 1988, he was a graduate student at Georgia Institute of Technology, receiving the Ph.D. in 1988. His research was in the formal modeling of communication protocols for computer networks. Since September 1988, he has been an Assistant Professor of computer science at the U.S. Naval Postgraduate School in Monterey, CA. He teaches classes and performs research in computer networks and communications. Raymond E. Miller received his Ph.D. degree from the University of Illinois, Urbana-Champaign, in 1957. He was a Research Staff Member at IBM Thomas J. Watson Research Center, Yorktown, Heights, NY, from 1957 to 1980, Director of the School of Information and Computer Science at Georgia Tech from 1980 to 1987, and is currently a Professor of Computer Science at the University of Maryland, College Park, and Director of the NASA Center of Excellence in Space Data and Information Sciences at Goddard Space Flight Center. He has written over 90 technical papers in areas of theory of computation, machine organization, parallel computation, and communication protocols. Dr. Miller is a Fellow of the American Association for the Advancement of Science, a Fellow of the IEEE and a member of ACM. Among his numerous society activities he served as an ACM Council Member-at-Large from 1976–1982, Editor in Chief of the Journal of the ACM from 1972–1976, a Board Member of the Computing Research Association from 1983–1991, and President of the Computing Sciences Accreditation Board from 1985–1987. Currently he is a member of the Board of Governors of the IEEE Computer Society and Vice President for Educational Activities.This research was performed while the authors were at Georgia Institute of Technology     

The construction of self-synchronizing finite state protocols

A technique is presented for constructing a finite state protocol from an originally given finite state specification of one process. We present three constructions, showing that they each provide send-receive symmetric solutions which are selfsynchronizing. Two lemmas are proved that provide insight into the types of interactions that arise in these types of finite state protocols. In essence we show that interactions occur between the processes only through isomorphic transitions and that during any interaction between the processes at most one of the two FIFO queues of messages is nonempty.Raymond E. Miller has been Director and Professor of the School of Information and Computer Science at the Georgia Institute of Technology since 1980. Prior to that he was employed by IBM for over thirty years, most of this time as a Research Staff Member at the IBM Research Center in Yorktown Heights, N.Y., where he held a number of technical management positions. He received a B.S. in Mechanical Engineering from the University of Wisconsin, Madison, and a B.S. in Electrical Engineering, M.S. in Mathematics, and PhD in Electrical Engineering, all from the University of Illinois, Urbana. His research areas of interest include theory of computation, machine organization, parallel computation, and communication protocols. He has written over sixty papers, authored a two volume book on switching theory, served as editor for a book on computer complexity, and is editor of a book series of foundations of computer science. He is a Fellow of the IEEE, a member of ACM and AAAS and has been active in numerous ACM capacities including being a member of the ACM Council for six years, an ACM National Lecturer for 1982–83, and a member of the AFIPS Board of Directors for four years. He is a member of the Computer Science Board, and was a member of the NSF Advisory Committee for Computer Research from 1982 to 1985, serving as Chairman for 1983–84. He has taught in a visiting or part time capacity at numerous institutions including Cal Tech, New York University, Yale, University of California at Berkeley and the Polytechnic Institute of New York.This work was partially supported through a contract with GTE Laboratories     

Improving the compression and encryption of images using FPGA-based cryptosystems

Compression and encryption technologies are important to the efficient solving of network bandwidth and security issues. A novel scheme, called the Image Compression Encryption Scheme (ICES), is presented. It combines the Haar Discrete Wavelet Transform (DWT), Significance-Linked Connected Component Analysis (SLCCA), and the Advance Encryption Standard (AES). Because of above reason the ICES efficiently reduce the overall processing time. This study develops a novel hardware system to compress and encrypt an image in real-time using an image compression encryption scheme. The proposed system exploits parallel processing to increase the throughout of the cryptosystem for Internet multimedia applications to implement the ICES. Using hardware acceleration for encryption and decryption, the FPGA implementation of DWT, SLCCA and the AES algorithm can be used. Using a pipeline structure, a very high data throughput of 330 Mbit/s at a clock frequency of 40 MHz was obtained. Therefore, the ICES is secure, fast and suited to high speed network protocols such as ATM (Asynchronous Transfer Mode), FDDI (Fiber Distributed Data Interface) or Internet multimedia applications. Shih-Ching Ou is working with the Department of Electrical Engineering, National Central University as a senior professor. His research interests include computer aided design, e-learning system, and virtual reality, etc. In August 2004, he serves as Leader University Professor and Director of Research and Development, now he act as Leader University Professor and Institute of Applied Information (Chairman). He has published a number of international journal and conferences papers related to these areas. Currently, he is the chief of Bioinformatics & CAD Laboratory. Hung-Yuan Chung joined the Department of Electrical Engineering at the National Central University, Chung-li, Taiwan as an associate professor in August 1987. Since August 1992, he was promoted as professor. In addition, he is a registered professional Engineer in R. O. C. He is a life member of the CIEE and the CIE. He received the outstanding Electrical Engineer award of the Chinese Institute of Electrical Engineering in October 2003. His research and teaching interests include System Theory and Control, Adaptive Control, Fuzzy Control, Neural Network Applications, and Microcomputer-Based Control Applications. Wen-Tsai Sung is a PhD candidate at Department of Electrical Engineering, National Central University in Taiwan. His research interests include computer aided design, web-based learning system, bioinformatics and virtual reality. He has published a number of international journal and conferences papers related to these areas. He received a BS degree from the Department of Industrial Education, National Taiwan Normal University, Taiwan in 1993 and received a MS degree from the Department of Electrical Engineering, National Central University, Taiwan in 2000. He has win the dragon thesis award; master degree thesis be recognized the most outstanding academic research. The thesis entitle is: “Integrated computer graphics system in a virtual environment.” Sponsor is Acer Foundation (Acer Universal Computer Co.). Currently, he is studying PhD at the Department of Electrical Engineering, National Central University as a researcher of Bioinformatics & CAD Laboratory.     

Necessary and sufficient conditions for broadcast consensus protocols

Summary We consider consensus protocols in asynchronous distributed systems that are based on broadcast communication. We show that a necessary and sufficient condition for the existence of a deterministic consensus protocol is delivery of each broadcast message to at least (n+k+1)/2 processes in ann-process system subject tok crash failures with either eventual fair broadcasting or eventual full broadcasting. The broadcast model captures the idea of a broadcast communication medium, such as the Ethernet, in which messages, if delivered, are delivered immediately and in order but not necessarily to all processes. Louise E. Moser received the Ph.D. degree in mathematics from the University of Wisconsin, Madison, in 1970. From 1970 to 1987 she was a professor of mathematics and computer science at California State University, Hayward. In 1987 she moved to the University of California, Santa Barbara, where is currently on the faculty of the Department of Electrical and Computer Engineering. Her current research interests include parallel and distributed systems, network architectures and communication protocols, and formal methods in software engineering. P.M. Melliar-Smith received the Ph.D. degree in computer science from the University of Cambridge, Cambridge, England, in 1987. He was a senior research scientist and program director at SRI International in Menlo Park (1976–1987), senior research associate at the University of Newcastle Upon Tyne (1973–1976), and principal designer for GEC Computers Ltd. in England (1964–1973). He is currently a professor in the Department of Electrical and Computer Engineering at the University of California, Santa Barbara. His research interests include fault-tolerant distributed systems, high-speed communication networks and protocols, and formal specification and verification. Vivek Agrawala received the B.Tech. degree in chemical engineering in 1984 and the M. Tech. degree in computer technology in 1986, both from the Indian Institute of Technology, Delhi, and a Ph.D. in computer science in 1991 from the University of California, Santa Barbara. Since then he has been a Research Scientist at Siemens Corporate Research, Princeton, New Jersey. His major research interests are distributed algorithms, software design methods, and distributed systems.This research was supported by the National Science Foundation, Grant Numbers CCR-8908515 and NCR-9016361. V. Agrawala's current address is Siemens Corporate Research, 755 College Road East, Princeton, NJ 08540, USA     

Parallel directed graph algorithms on directional processor arrays with reconfigurable bus systems

Processors arrays with reconfigurable bus systems (abbreviated to PARBS) have been received a lot of attention in the last decade, and many undirected graph algorithms with constant time complexity have been proposed on PARBS. However, for a directed graph, it will be proved that connecting PARBS in the way proposed for undirected graphs generates paths which do not exist in the directed graph. This result may lead to incorrect solution for directed graph problems. Therefore, in this paper, a model named D-PARBS (Directional PARBS) is proposed for eliminating the non-existent paths. This model can be used to correctly identifying redundant arcs on directed graphs in constant time. Furthermore, by modifying the D-PARBS architecture, constant time algorithms with O(n ³) processors are developed to solve topological sort, transitive closure, cyclic graph checking, and strongly connected component problems on directed graphs. Chi-Jung Kuo: He is currently an operation officer of the Information Processing Department in the Taipei Branch of Bangkok Bank. His research interests include parallel processing and graph theory. He received his B.S. and M.S. degree in Information Management from National Taiwan University of Science and Technology in 1993 and 1995, respectively. He was a teacher in the Chin Min Junior College from 1995 to 1996. Chiun-Chieh Hsu, Ph.D.: He is currently a full professor of Information Management Department at National Taiwan University of Science and Technology. His current research interests include fault-tolerant computing, parallel and distributed processing, networks, and graph theory. He received his B.E., M.E., and Ph.D. degrees all in Electrical Engineering from National Taiwan University in 1983, 1987, and 1990, respectively. He worked as a software and firmware design engineer of Research and Development in Acer Computer Company from 1983 to 1985. Wei-Chen Fang: He received the BS degree in MIS from Tamkang University and the MS degree in Information Management from National Taiwan University of Science and Technology. Currently, he is a Ph.d student and works as an assistant researcher with the Advanced Technology research group for Chunghwa Telecommunication Laboratory. His research interests include multi-processor architecture, fault-tolerant computing, and parallel and distributed processing.     

Reliable broadcasts and communication models: tradeoffs and lower bounds

Reliable Broadcast is a mechanism by which a processor in a distributed system disseminates a value to all other processors in the presence of both communication and processor failures. Protocols to achieve Reliable Broadcast are at the heart of most fault-tolerant applications. We characterize the execution time of Reliable Broadcast protocols as a function of the communication model. This model includes familiar communication structures such as fully-connected point-to-point graphs, linear chains, rings, broadcast networks (such as Ethernet) and buses. We derive a parameterized protocol that implements Reliable Broadcast for any member within this class. We obtain lower bound results that show the optimality of our protocols. The lower bound results identify a time complexity gap between systems where processors may only fail to send messages, and systems where processors may fail both to send and to receive messages. The tradeoffs that our results reveal between performance, resiliency and network cost offer many new alternatives previously not considered in designing fault-tolerant systems. Özalp Babaoglu is Associate Professor in the Department of Computer Science at Cornell University, Ithaca, New York. His research interests include distributed systems, fault tolerance, performance evaluation and modeling. He received a BS in electrical engineering from George Washington University, Washington, D.C. in 1976. From the University of California, Berkeley, he received a MS in 1977 and a PhD in 1981, both in computer science. While at Berkeley, he designed and implemented the virtual memory extensions to VAX Unix that came to be known as 3. Obsd. Pat Stephenson is a Doctoral Candidate in the Computer Science Department at Cornell University, Ithaca, New York. His research interests include distributed systems and fault tolerance. In 1983, he received a B.A. (Mod.) in computer science from Trinity College, Dublin, Ireland. He received his MS in computer science from Cornell in 1986. He is currently working on new tradeoffs in the design of fault-tolerant algorithms. Rogério Drummond is Assistant Professor in the Computer Science Department at the Universidade Estadual de Campinas (UNICAMP), São Paulo, Brazil. His interests include distributed computing, fault tolerance and operating systems. He received a BS and a MS in computer science from the Universidade Estadual de Campinas in 1978 and 1980, respectively. In 1986 he received a PhD in computer science from Cornell University. He is currently working on integrated environments for the development of software and hardware.Partial support for this work was provided by the National Science Foundation under Grants DCR-86-01864 and MCS-82-10356 and AT&T under a Foundation GrantSupported partially by the Defense Advanced Research Projects Agency (DoD) under ARPA order 5378, Contract MDA 903-85-C-0124, and partially by an IBM graduate fellowship. The views, opinions and findings contained in this report are solely those of the authors and should not be construed as an official Department of Defense position, policy, or decisionSupported partially by the CAPES and CNPq agencies of the Ministry of Education of Brazil     

Bounded time-stamps

Summary Time-stamps are labels which a system adds to its data items. These labels enable the system to keep track of the temporal precedence relations among its data elements. Many distributed protocols and some applications use the natural numbers as time-stamps. The natural numbers however are not useful for bounded protocols. In this paper we develop a theory ofbounded time-stamps. Time-stamp schemes are defined and the complexity of their implementation is analyzed. This indicates a direction for developing a general tool for converting time-stamp based protocols to bounded protocols. Amos Israeli received his B.Sc. in Mathematics and Physics from Hebrew University in 1976, and his M.Sc. and D.Sc. in Computer Science from the Weizmann Institute in 1980 and the Technion in 1985, respectively. Currently he is a senior lecturer at the Tlectrical Engineering Department at the Technion. Prior to this he was a postdoctoral fellow at the Aiken Computation Laboratory at Harvard. His research interests are in Parallel and Distributed Computing and in Robotics. In particular he has worked on the design and analysis of Wait-Free and Self-Stabilizing distributed protocols. Ming Li received his M.S. and Ph.D. in Computer Science from Wayne State University in 1980 and Cornell University 1985, respectively. Currently he is an associate professor at the Computer Science Department at the University of Waterloo. His research interests are in Theory of Computing, Kolmogorov Complexity, and Machine Learning.Supported in part by the Weizmann fellowship and NSF Grant DCR-86-00379Supported in part by ONR Grant N00014-85-k-0445 and Army Research Office Grant DAAL03-86-K-0171 at Harvard University, by NSF Grant kDCR-86-06366 at Ohio State University, and by NSERC Operating Grant OGP0036747. Most of this work was done when the authors were at Aiken Computation Laboratory at Harvard University. The authors also acknowledge the hospitality of the computer science department at York University, Canada