Introduction to Discrete-Systems Theory

Instructor: Luca de Alfaro

2pm-3:45pm, Tuesdays and Thursdays
Social Sciences 2

Office Hours: 1-2, Tuesdays, or by appointment
Email: luca@soe.ucsc.edu

The course provides an introduction to the modeling, specification, verification and analysis of discrete-state systems. The application areas range from hardware design, to embedded systems, and to real-time systems. The course will also provide a brief overview of techniques for software verification.

Lecture Notes

• October 14, 2003 (postscript, pdf).
• October 16, 2003 (postscript, pdf).
• October 31, 2003 (postscript, pdf).
• November 6, 2003 (postscript, pdf).

Readings and Homework

• 9.30.2003
  • Main reading: L. de Alfaro: Games as a Model for Open Systems.
  • Additional reading:
    • L. de Alfaro, T.A. Henzinger: Interface Automata (except sections 4 and 5). This is the paper where interface automata were introduced.
    • L. de Alfaro, M. Stoelinga: Interfaces: A Game-Theoretic Framework to Reason about Component-Based Systems (sections 1 and 2 only). This is another good introduction to interface automata.
    • N.A. Lynch, M.R. Tuttle: Hierarchical Correctness Proofs for Distributed Algorithms. This is the paper where I/O automata were introduced.
    • N.A. Lynch, M.R. Tuttle: An Introduction to Input/Output Automata. This is a standard introduction to I/O automata.
• 10.14.03
  • Reading: in the Lecture Notes (postscript, pdf) read pages 23 and 24 (not section 4.2); also, read pages 29, 30, 31, and 32, stopping before section 4.3.3.2.
  • Homework due October 21:
    • Problem 6 page 29
    • Problem 8 page 30
    • Instead of Problem 9 page 30, you can do problem 14 at page 34 of the October 16 Lecture Notes.
    • Problem 11 page 31
    • Problem 12 page 32
    Every problem is worth 20 points, for a total of 100.
• 10.30.03
  • Reading: In the Lecture Notes (postscript, pdf) read Chapter 2 (Automata) and Chapter 6 (Alternating Relations).
  • Review: This is a good time to review the lecture notes: you should be famiiar with all their content (as of the October 31 version).
  • Homework due November 6:
    • Chapter 2 problems 4, 5, 6, 7
    • Chapter 5 problems 23, 24.
• 11.06.03
  • Reading: In the Lecture Notes (postscript, pdf) read Chapter 7, and start reading Chapter 8 (we will finish discussing Chapter 8 in class).
• 11.13.03
  • Reading: Read chapter 4: Symbolic graph representation (postscript, pdf) of the book draft Computer Aided Verification by Tom Henzinger and Rajeev Alur.
• 11.17.03
  • Reading: Read chapter 8 of the lecture notes.
  • Homework 3, due Thursday November 20.
  • Homework 4, due Tuesday November 25.
• 12.1.03
  • Homework 5, due on final's day.

Prerequisites

Homework, Final

The course will have a final exam.

Tools

• Mocha/Chai. Mocha is a verification tool similar in the basic ideas to the commercial tools of Synopsis, Intel, Cadence, and other companies, but open source, and thus open to experimentation. We have available Chai, an advanced version of Mocha, that enables the analysis of both transition systems and games.
• Flexi. Flexi is a verification tool designed to help in component-based design. You can create small automata that describe system components, check that they are compatible, put them together to forme larger designs, and verify that the designs work correctly. This tools has been developed by the instructor's research group. Sorry, URL coming soon.

Syllabus

• Introduction.
• System models: transition systems and games.
• Simple transition systems and game problems: safety and reachability. How to verify safety and reachability properties.
• Languages for describing transition systems and games. Approaches based on automata, and on state variables. Efficient representations for complex systems.
• Efficient algorithms for reachability and safety problems: BDDs, BDD operations, and symbolic algorithms.
• How can we compose system models to create models of complex, modular systems? Compostion for transition systems, and for games.
• Specification languages: temporal logic, automata, and fixpoint logics.
• System relations: equivalence relations (when are two systems equivalent?), and implementation relations (when does a system implement another? When can we substitute a component for another in an implementation?).
• Extensions to the analysis of quantitative properties: timing, reliability, performance, quality of service, cost.
• Verification in industrial practice: current approaches to microprocessor and embedded system verification.
• Overview of software verification techniques.