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.