Officially, the course will be an independent project (e.g., CS399 (Independent project) or CS399P), and students will be graded on the basis of their project work. In addition, there will be five lectures in the first part of the quarter about software testing and the "software model-checking" approach in particular. The project is described in more detail below.
Current plans are to schedule the lectures on Thursday from 9 AM to Noon. If you are seriously interested in taking the course and have an unresolvable conflict at that time, please send me email (dill@cs.stanford.edu).
This should be of appropriate for graduate students or advanced undergrads. The only prerequisite is that you be very comfortable programming in C on Unix.
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.
Part1: models, steps, roles, tools. Part2: more detailed presentation on analysis and testing.
Sep 30: Lecture 2: Communication Software
Part1: key features, methods and tools for dealing with concurrency and real-time. Part2: model-checking and VeriSoft.
Oct 14: Lecture 3: Model-Checking Software with VeriSoft
Part1: what is VeriSoft, how to use it, examples of applications, strengths and limitations. Part2: advanced features, dealing with complexity. 1st exercises with VeriSoft.
Oct 21: Lecture 4: Inside VeriSoft
Architecture, reactive semantics, state explosion, partial-order methods, libraries of communication objects. Review 1st exercises.
Oct 28: Lecture 5: Project Description: Design and Testing of Internet Phones
Introduction to (internet) telephony, problem description, programming environment, assumptions (API), project milestones, getting started.