Massachusetts Institute of Technology Handout 4 6.897: Modeling and Analyzing Really Complicated Systems, Using State Machines Profs. Nancy Lynch, Daniel Jackson, and Michael Ernst February 6, 2001

6.897 Schedule: Version 1

Lecture 1 Tuesday, February 6 Lynch Overview; State machines, invariants, and levels of abstraction

Lecture 2 Thursday, February 8 Lynch Other views of state machines, invariants, and abstraction: Manna, Pnueli, and Lamport

Lecture 3 Tuesday, February 13 Lynch Abstraction relations; Statecharts Due: Hand in choice of case study area

Lecture 4 Thursday, February 15 Lynch Model-checking overview

Lecture 5 Thursday, February 22 ??? SPIN model-checker

Lecture 6 Tuesday, February 27 ??? TLC model-checker

Lecture 7 Thursday, March 1 Ernst Invariant discovery

Lecture 8 Tuesday, March 6 Garland Theorem proving

Lecture 9 Thursday, March 8 Garland Theorem proving, LP

Lecture 10 Tuesday, March 13 Garland Theorem proving, LP, IOA

Lecture 11 Thursday, March 15 Lynch Simple systems: liveness Lecture 12 Tuesday, March 20

Attie Liveness, temporal logic

Lecture 13 Thursday, March 22 Lynch Composition

Lecture 14 Tuesday, April 3 Lynch, Attie Composition, dynamic systems

Lecture 15 Thursday, April 5 Attie, Jackson Dynamic systems, relational models

Lecture 16 Tuesday, April 10 Jackson Relational models

Lecture 17 Thursday, April 12 Lynch Timed systems

Lecture 18 Thursday, April 19 Lynch Timed systems

Lecture 19 Tuesday, April 24 Alur Timed systems, Uppaal

Lecture 20 Thursday, April 26 Lynch Timed systems

Lecture 21 Tuesday, May 1 Lynch Hybrid systems

Lecture 22 Thursday, May 3 Lynch Hybrid systems

Lecture 23 Tuesday, May 8 ??? Hytech

Lecture 24 Thursday, May 10 Lynch Hybrid systems Lecture 25 Tuesday, May 15

Lynch Probabilistic systems

Lecture 26 Thursday, May 17 Lynch Probabilistic systems Due: Hand in final “portfolio” of case study examples