CSSE373 – Formal Methods in Specification and Design

Spring 2010

Schedule Overview

Schedule subject to revision. Readings should be completed before class on the session listed. Homework is due before 6 a.m. on the date listed. Projects are due before midnight on the date listed. Homework and projects should be submitted by committing the required documents to your individual or team SVN repository. Unless otherwise specified, documents must be submitted in pdf format. See the syllabus for details on the late policy.

Schedule last updated Sun May 16.

Session quick links:  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40

Week Session HW Due 6am Proj. Due 11:55pm Reading Quiz Handout Topic
1

1

Mon Mar 8

     Q1   Introduction
1

2

Tue Mar 9

     Q2   What are formal methods? BRING LAPTOPS
1

3

Thu Mar 11

 HW1         No class, Curt gone to SIGCSE
1

4

Fri Mar 12

           No class, Curt gone to SIGCSE
2

5

Mon Mar 15

    
  • Ch. 2
     BRING LAPTOPS AND TEXT BOOK – Getting Started with Alloy
2

6

Tue Mar 16

    
  • Ch. 3.1–3.3
 Q3   Logic of Alloy
2

7

Thu Mar 18

 Alloy Lab  
  • 3.4
 Q4   Alloy operators
2

8

Fri Mar 19

    
  • 3.5–3.7
 Q5   Alloy constraints
3

9

Mon Mar 22

 HW2  
  • 4.1–4.2
 Q6   Intro. to the Alloy modeling language
3

10

Tue Mar 23

    
  • 4.3–4.4
 Q7   Alloy fields and types
3

11

Thu Mar 25

 HW3  
  • 4.5–4.6
 Q8   Alloy paragraphs and commands
3

12

Fri Mar 26

    
  • 4.7–4.8
 Q9   Reuse and arithmetic in Alloy
4

13

Mon Mar 29

 HW4  
  • Ch. 5
 Q10   Analysis
4

14

Tue Mar 30

   P1       No class, project work day
4

15

Thu Apr 1

    
  • 6.1–6.2
 Q11   Alloy examples
4

16

Fri Apr 2

 HW5  
  • 6.3–6.4
     More Alloy examples
5

17

Mon Apr 12

           Alloy Review
5

18

Tue Apr 13

 HW6         No class, project work day
5

19

Thu Apr 15

           EXAM 1
5

20

Fri Apr 16

   P2       No class, project work day
6

21

Mon Apr 19

     Q12   Introduction to JML and Formal Verification
6

22

Tue Apr 20

     Q13   More Program Verification—statements
6

23

Thu Apr 22

 HW7     Q14   Program verification—notation
6

24

Fri Apr 23

           Optional program verification practice
7

25

Mon Apr 26

 HW8   Q15   Program verification—methods
7

26

Tue Apr 27

     Q16   Program verification—recursion
7

27

Thu Apr 29

     Q17   Data modeling with JML
7

28

Fri Apr 30

         Data modeling with JML (cont.)
8

29

Mon May 3

 HW9     Q18   Representation Hiding in JML
8

30

Tue May 4

           No class, project work day
8

31

Thu May 6

 HW10         Review
8

32

Fri May 7

           EXAM 2
9

33

Mon May 10

   P3   Q19   State diagrams
9

34

Tue May 11

     Q20 Traffic Light Statecharts
9

35

Thu May 13

       Q21   Higher-order statecharts
9

36

Fri May 14

 HW11 (No Late Days!)         No class, pick up Take-home EXAM 3 from my office before 4:30 p.m. (Exam due at start of class on Monday)
10

37

Mon May 17

     Q22   State of the practice in formal methods, course evaluations
10

38

Tue May 18

           No class, project work day
10

39

Thu May 20

 HW12         No class, project work day
10

40

Fri May 21

   P4       No class, project work day