Enrollment and prerequisites:
PhD and MS students in EECS; others (for example, MEng students in EECS and graduate students in other departments) with permission of one of the instructors. Students should have a strong background in mathematics, plus a good knowledge of computer systems (e.g., 6.033) and algorithms (e.g., 6.046).
Executive summary:
This course will explore the available state-machine-based methods for modeling and analyzing complex systems and will attempt to determine what is needed to make them more useful in practice. Students will study and learn to use a broad set of modeling techniques and analysis tools, and will apply them to case studies in areas such as data management in distributed networks, reliable network communication, mobile computing, automated transportation, and object-oriented programming.
Background:
Computer systems are becoming increasingly pervasive and increasingly complicated. The applications that are being constructed are becoming more ambitious (consider group games, support for military operations, electronic commerce, automated transportation, on-line data repositories,...). At the same time, the environments in which the systems must operate are becoming more dynamic (consider network changes, mobility, participants joining and leaving, failures,...). This combination leads to very complex systems, which can be hard to build and hard to understand.
One approach to making complex systems easier to build and understand is to develop precise system models and to try to use them in the system development process. These models can be used for documentation, for informal and formal arguments about correctness, and for performance analysis and prediction. Most of the popular models nowadays are based on some form of ``state machines'', which describe systems in terms of states and transitions.
Course overview:
In this new graduate course, we will explore the available state-machine-based methods for modeling and analyzing complex systems and will attempt to determine what is needed to make them more useful in practice.
We will study the mathematical foundations in depth, will learn the principles and usage of several support tools (model checker(s), theorem prover(s), an invariant generator,...), and will apply the mathematics and the tools to examples from several application domains. We will try to understand both the theory behind the models and methods, and how they can be used in practice.
The application domains currently being considered as focus areas are:
These choices might be adjusted, depending on the interests of the participants. Individual students will choose particular focus areas.
This course will have an interactive style---it won't be just a series of lectures. The class size should be small enough to allow everyone to participate actively. Students will be expected to read assigned papers and (parts of) books ahead of time, participate in discussions, and help to present some of the material. They will be expected to learn about, use, and teach others about, several tools, and to help develop a ``library'' of case study examples based on the application areas. Two kinds of examples will be developed: small toy examples to illustrate the use of the methods, and more elaborate examples that capture some of the interesting difficulties of the target application domains.
The class may split up into teams based on interest in the particular target application areas. The whole class will read and discuss the same papers and learn about the same tools. Different groups may apply the methods to different examples.
We hope to bring in some outside experts to participate in (or lead) some of the class meetings.
Partial course outline:
I. Monolithic Asynchronous Systems, Safety Properties
II. Monolithic Asynchronous Systems, Liveness Properties
III. Asynchronous Systems with Composition
IV. Timed Systems
V. Hybrid (continuous/discrete) Systems
VI. Probabilistic Systems