CMPE 293 Home Page
Fall 2001
Fall 2001 Topic:
Introduction to Discrete-Systems Theory
2pm-3:45pm, Tuesdays and Thursdays
Crown College, Rm 105
We are designing ever more complex software and hardware systems.
- How do we split a design in components that can be implemented
independently?
- How can we ensure that the components, once put together, work
together?
- How can we analyze and check a design before we actually
implement it?
- What is the mathematical meaning of "composition",
"implementation", and "hierarchy"?
These are the topics of CMPE 293 this fall. CMPE 293 will present a
graduate-level introduction to the methods for modeling, analyzing,
and reasoning about discrete systems, such as hardware and software
designs. The first part of the course will present basic models for
hardware and software systems, and will introduce methods for system
specification, verification, abstraction, and stepwise refinement of a
design into an implementation. The second part of the course will
discuss the role of structure: hierarchy, system composition and
interface specification.
There is no textbook for the course: reading material will be
indicated or distributed during the course. There is no prerequisite
for this course, but some mathematical background will be assumed.
Announcements
- No class on Tuesday, October 9.
I am attending the EMSOFT 2001 conference (Embedded Software).
Office Hours
Mondays, 1:30-2:30, and Thursdays, 12:00-1:00.
Handouts
Lecture Notes
The Mocha
Model Checker
R. Alur and T.A. Henzinger. Computer Aided Verification.
The "CAV" book, posted with permission from the authors.
Assigned Readings
- Tuesday October 4, 2001. Chapters 0, 1, 2 of the
lecture notes, and Chapter 4 of the CAV book.
Papers
- Model
Checking for Programming Languages using Verisoft. Look also at
the web page of Patrice
Godefroid for related work.
- Zohar Manna and Amir Pnueli. Temporal Verification Diagrams. In
International Symposium on Theoretical Aspects of Computer Software,
Lecture Notes in Computer Science 789, Springer-Verlag, pp. 726-765,
1994.
Postscript,
PDF.
- L. de Alfaro, Z. Manna, H.B. Sipma, T. Uribe.
Visual Verification of Reactive Systems.
In TACAS 97: 3rd International
Worskshop on Tools and Algorithms for the Construction and Analysis of
Systems, Lectures Notes in Computer Science 1217,
pages 334-350, Springer-Verlag, 1997.
Postscript,
PDF.
- Nikolaj Bjørner, I. Anca Browne and Zohar Manna.
Automatic
Generation of Invariants and Intermediate Assertions.
Theoretical Computer Science, vol. 173(1), pp. 49-87, February
1997. Original version appeared in 1st International Conference on
Principles and Practice of Constraint Programming, Lecture Notes in
Computer Science 976, Cassis, France, pp. 589-623, September 1995.
Homeworks
Other Information
Luca de Alfaro
luca@soe.ucsc.edu
Office: Baskin 317A
Phone: (831) 459-4982