Design and Analysis of Communication Software

Stanford University, Fall Quarter 1999

Course CS399, given by Patrice Godefroid in collaboration with Prof. David L. Dill.

Course Description

Communication software coordinates the information flow between interconnected components in the multitude of networks that are ubiquitous in our lifes: the internet, the telephone network, wireless systems and pagers, banking networks, distributed databases, etc. Communication software is notably hard to design and test because communicating entities may interact in many unexpected ways.

This experimental course will provide an introduction to the design and analysis of communication software from a fresh perspective. The course will present a brief overview of existing practices and tools used in industry for developing software and communication software in particular. The course will focus on practical analysis techniques and tools currently available to the software developer, and will discuss their strengths and limitations.

Then we will present a new approach for automatically analyzing communication software based on the use of systematic state-space exploration techniques, also known as "model-checking". The ideas developed in this part will be illustrated using VeriSoft, a new tool for systematically testing concurrent reactive software systems. VeriSoft integrates automatic test generation, execution and evaluation in a single framework, and can quickly reveal behaviors that are virtually impossible to detect using conventional testing techniques. This approach has been applied successfully for analyzing (testing, debugging, reverse-engineering) several software products developed in Lucent Technologies.

Finally, participants will experience first-hand the concepts described previously in the course by designing, implementing and testing a simple but realistic example of communication software. Specifically, simple software "internet phones" will be developed in C/C++ using a predefined platform (UNIX, TCP/IP, given API for recording and playing sounds). The exercise will focus on the development and testing of the call processing and signalling aspects of the problem. This part will expose the participants to basic notions of internet telephony.

Time slots: Thursday, 9AM-11:50AM, Gates B12

Schedule:

Lecture Notes

Lecture 1 (pdf)
Lecture 2 (postscript)
Lecture 3 (postscript)
Lecture 4 (postscript)
Lecture 5 (pdf)
Project Description (postscript)