Quick Links: [ What's New | Staff | Timetable | Part 1 | Part 2 | Outlines ]

COMP424/524-06A: Topics in Software Engineering

What's New

• COMP524-06A Projects. The final projects are due on Wednesday 5th July 2006.

Lecturers

Steve Reeves			Robi Malik
Office:	G 1.23		Office:	G 2.03
Phone:	07 838 4398		Phone:	07 838 4796
e-Mail:			e-Mail:

Timetable

Part I: Finite State Machines (Robi Malik)

The lecture handouts are the slides which will be presented in class: each file corresponds to one lecture. They are as accurate as possible at the time of publishing. However, if errors are detected, handouts may be changed without notice until shortly after each lecture.

Week 1-2: Finite State Machines

Here are the handouts for the lectures.

1. Reactive Systems
2. Automata and Languages
3. Synchronous Product
4. Supervisory Control
5. Blocking
6. Controller Synthesis

More comprehensive material can be found in the textbook, of which we will cover chapter 1 in these two weeks.

• B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, Ph. Schnoebelen, Model-Checking Techniques and Tools. Springer, 1999.
• W. M. Wonham, Notes on Control of Discrete Event Systems. [Online from Campus]

And here are the example models to be presented in class.

• Transfer Line
• Cat and Mouse
• Tic-Tac-Toe

Assignment 1 was due on Monday 13th March 2006.

• Please collect your marked scripts from the school reception G G.20.
• Task description
• Plant model for exercise 2
• Frequently Asked Questions

Week 3-4: CTL Model Checking

Here are the handouts for the lectures.

1. Temporal Logics
2. Introduction to SMV
3. Computation Tree Logics
4. Safety Properties
5. Liveness Properties
6. Fairness Assumptions

Here are some example SMV models to be presented in class.

• Underground Management System
• Alternating Bit Protocol using CTL
• Alternating Bit Protocol using PLTL

Assignment 2 was due on Monday 27th March 2006.

• Please collect your marked scripts from the school reception G G.20.
• Task description
• NuSMV model of elevator for exercise 2
• Frequently Asked Questions
• NuSMV homepage
• NuSMV 2.3 manual (PDF from campus)
• NuSMV 2.3 tutorial (PDF from campus)

Week 5-6: Model Checking Algorithms

Here are the handouts for the lectures.

1. State Exploration
2. Implementation Issues
3. Binary Decision Diagrams
4. Model Checking CTL
5. Symbolic Model Checking
6. Incremental Verification

Here are some links to common OBDD packages.

• Buddy
• CUDD
• JDD

Assignment 3 was due on Monday 10th April 2006 at 9:00 A.M.

• Please collect your marked scripts from the school reception G G.20.
• Task description
• Download the Waters Automata Toolkit:
  • GZIP'ed TAR archive (1915 kB)
  • ZIP archive (2811 kB)
• There was a BUG in the Waters Toolkit. Please us the new archive which has now been uploaded. You can also patch your distribution with this new version of waters424.jar.
• Waters API Documentation (Only accessible when on campus)

Part II: Specification and Refinement in Z (Steve Reeves)

• The PDF file for the textbook I shall be using for the second half of the course is here. Please note this is a VERY LARGE file so don't try printing it all unless you have lots of money to spare!!

• Here are the slides for the start of the course---these were produced by the authors of the textbook, and I shall be working through some of this, but leaving it to you, over the break, to cover this material for yourselves. It is really revision for you all since you've covered logic, sets, functions etc. in previous years.

COMP524-06A Projects

The COMP524-06A Projects are due on Wednesday 5th July 2006 at 11:00 A.M.

• Task description
• Download the Example Mazes:
  • GZIP'ed TAR archive (1915 kB)
  • ZIP archive (2811 kB)
• Project meetings will be held every Wednesday at 11:00 in G 1.15.

Course Outlines

• COMP424-06A Course Outline [HTML] [PDF]
• COMP524-06A Course Outline [HTML] [PDF]

Robi Malik, Department of Computer Science, The University of Waikato;
Last modified: 23 Jun 2006