CSSE373 – Formal Methods in Specification and Design

Spring 2009

Schedule Overview

Schedule under construction and subject to revision. Readings should be completed before class on the session listed. Homework and 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 17.

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 Due Reading Quiz Handout Topic
1

1

Mon Mar 9

   Q1   Introduction
1

2

Tue Mar 10

 HW1 Q2   What are formal methods?
1

3

Thu Mar 12

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

4

Fri Mar 13

 Alloy Lab       BRING LAPTOPS AND TEXT BOOK – More Alloy lab time
2

5

Mon Mar 16

  
  • Ch. 3.1–3.3
 Q3   Logic of Alloy (convocation schedule class starts 10 minutes late)
2

6

Tue Mar 17

 HW2
  • 3.4
 Q4   Alloy operators
2

7

Thu Mar 19

  
  • 3.5–3.7
 Q5   Alloy constraints
2

8

Fri Mar 20

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

9

Mon Mar 23

  
  • 4.3–4.5
 Q7   Alloy fields and types
3

10

Tue Mar 24

 HW4
  • 4.6–4.8
 Q8   Alloy paragraphs, commands, and reuse
3

11

Thu Mar 26

         No class, project work day
3

12

Fri Mar 27

 P1       No class, project work day
4

13

Mon Mar 30

  
  • Ch. 4.8
  • Ch. 5
 Q9   Alloy Integers, Analysis
4

14

Tue Mar 31

 HW5
  • 6.1–6.2
 Q10   Alloy examples
4

15

Thu Apr 2

  
  • 6.3–6.4
     More Alloy examples
4

16

Fri Apr 3

 HW6       No class, project work day
5

17

Mon Apr 6

         No class, project work day
5

18

Tue Apr 7

         Alloy Review
5

19

Thu Apr 9

         EXAM 1
5

20

Fri Apr 10

 P2       No class, project work day
6

21

Mon Apr 20

   Q11   Introduction to JML and Formal Verification
6

22

Tue Apr 21

 HW7 Q12   More Program Verification—statements
6

23

Thu Apr 23

     Q13   Program verification—notation
6

24

Fri Apr 24

 HW8       No class, “sun” day, program verification practice
7

25

Mon Apr 27

   Q14   Program verification—methods
7

26

Tue Apr 28

 HW9 Q15   Program verification—recursion
7

27

Thu Apr 30

   Q16   Data modeling with JML
7

28

Fri May 1

 HW10 Q17   JML Wrap-up
8

29

Mon May 4

 HW10       No class, project work day
8

30

Tue May 5

         Review
8

31

Thu May 7

         EXAM 2
8

32

Fri May 8

 P3   Q18   State diagrams
9

33

Mon May 11

   Q19 Traffic Light Statecharts
9

34

Tue May 12

 HW11   Q20   Higher-order statecharts
9

35

Thu May 14

         Review
9

36

Fri May 15

         EXAM 3
10

37

Mon May 18

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

38

Tue May 19

 HW12       No class, project work day
10

39

Thu May 21

         No class, project work day
10

40

Fri May 22

 P4       No class, project work day