IFIP TC6/WG 6.1 Joint International Conference on
Formal Description Techniques for Distributed System and Communication
Protocols and Protocol Specification; Testing and Verification
Beijing; China; October 5-8; 1999

8:00－17:00 Registration

9:00－17:00   Tutorial I (Full Day)
Assembly Room One

Stochastic Process Algebras: Linking Process Descriptions with Performance
Ed Brinksma,University of Twente, Netherlands

In this tutorial we will present an overview of the research on stochastic process algebras, a branch of process algebra that is a product of the last decade. Like ordinary process algebra, stochastic process algebra (SPA) provides a compositional model for the description and analysis of complex distributed systems, such as network protocol systems. At the same time SPAs are extended with stochastic features to enable the compositional and systematic derivation of performance models from such descriptions. In our tutorial we will discuss the motivation and potential benefits of the use of SPAs. We present the main issues in the development of SPAs, including theoretical complications and their solutions according to the different schools of thought. In particular, we will present so-called Markovian process algebras that allow for performance analysis in terms of Continuous Time Markov Chains (CTMC), as well as a non-Markovian process algebra enabling the use more general performance models. Late but not least, we give examples of the practical use of SPAs for protocol performance evaluation.

9:00－12:30    Tutorial II (Half Day)
Assembly Room Two

Model checking and Software Verification
Gerard Holzmann, Bell Labs, USA

Most existing model checkers were designed for the verification of clock-driven synchronous systems, manipulating bits and signals. These systems tend to perform poorly when applied to distributed software applications. Such systems are typically asynchronous, use several independent clocks, and manipulate higher level data structures that have little or no coherence at the bit-level. In this tutorial we show how a model checker can be optimized for software verification problems, and can be made to adjust itself to the limits of the physical hardware that it executes on. We will cover in detail the principles of on-the-fly model checking as they are built into the Bell Labs' model checker Spin. We will also give an overview of a recent large-scale application of Spin based model checking to the exhaustive verification of the software for a new telephone switch built at Lucent Technologies.

Dr. Gerard Holzmann received his Ph.D. in the technical sciences from the Delft University of Technology in The Netherlands in 1979. He has been with the Computer Science Research Center of Bell Labs since 1980. Dr. Holzmann wrote one of the first on-the-fly verification systems (Pan) in 1980. His well-known Spin model checker has been distributed by Bell Labs in source form since 1990.

13:30－17:00   Tutorial III   (Half Day)
Assembly Room Two

Traffic Control and QoS Management In the Internet
Hui Zhang, Carnegie Mellon University, USA

Due to the success of the Internet, we see two important trends: first, the internet is involving into a global and commercial communication infrastructure supporting applications with diverse traffic characteristics and performance requirements. Second, the Internet technology is becoming the technical basis for not only the Internet but also for most data communication networks, both public and private. To cope with emerging applications, business, and administrative requirements, new service models, resource management algorithms, and protocols have been developed in the last several years. They include improvements to TCP algorithms (Vegas, SACK, new Reno, NetReno, FACK), router mechanisms for congestion and traffic management (RED, Fair Queueing, ECN, TCP snooping, hierarchical link-sharing), service models, protocols, algorithms to support end-to-end QoS on a per flow basis (intserv, RSVP, traffic control, admission control, QoS routing), and more recently, service models and algorithms to support QoS for traffic aggregates (diffserv, WRED, traffic conditioning, provisioning). In this tutorial, we will give an overview of these algorithms,describe their mechanisms, and identify their strengths and weaknesses. Throughout the tutorial, we will discuss the architectural implications of the new algorithms/protocols/service models, including their impact on the following important goals for Internet: scalability, robustness, heterogeneity.

Biography

Hui Zhang is the Finmeccanica Assistant Professor at the School of Computer Science of Carnegie Mellon University. He received his Ph.D. degree in Computer Science from the University of California at Berkeley. Before joining the faculty at CMU in 1995, he spent one year at the Lawrence Berkeley National Laboratory as a Post Doctoral Fellow. Professor Hui Zhang has conducted research in the area of resource management algorithms and protocols for wide-area internetworks for the last ten years. His research includes scheduling, traffic characterization, admission control, routing, congestion control, reliable multicasting algorithms, and real-time protocols. He is on the Editorial Board of IEEE/ACM Transactions on Networking, ACM Computer Communication Review, and Computer Communications Journal. He has served on the program committees of most leading networking, real-time, and multimedia conferences including SIGCOMM, INFOCOM, ICNP, SIMETRICS, NOSSDAV, IWQoS, RTSS, RTAS, ACM Multimedia, and IEEE Multimedia. Professor Zhang received the National Science Foundation CAREER Award in 1996.