Software Specification (2IW05)

Lectures:
Instruction: There are instructions for two hours per week. There are two groups:
  1. Tim Willemse (English spoken), PT 2.19, Tuesdays 15:45-17:30 and
  2. Bas Luttik (Dutch spoken), PT 2.23, Tuesdays 15:45-17:30.
Note that the first instructions will be held on 08-09-2009.
Practical Project:

In order to avoid any interference with the exams, we do recommend that the students stick to the previously announced deadline for the delivery of their final project. However, Peach will be open for submissions (without any decrease in the mark) till January 22, 2010. The criteria for the evaluation of the final report of practical project can be found here.

The goal of the project is to specify a software system for a "Laptop WebShop". Project description, deliverables and deadlines can be found here. The deliverables should be handed in to the instructors and they will provide you with feedback.


Material:
Exams: The exams are closed book, meaning that during the exams it is not allowed to use the lecture notes, the slides, or your own notes.
Agenda:

date topics slides exercises
lecture 1
September 1, 2009
Introduction to Software Specification
Use Case Diagrams
Introduction Use Cases none (no instructions)
lecture 2
September 8, 2009
Class Diagrams
Case Studies
Class Diagrams and Case Studies 2.5.1-3
3.3.1-4
lecture 3
September 15, 2009
Z Z: Introduction, Definitions, Schemas 4.2.1-6
4.4.1-2
lecture 4
September 22, 2009
Z Z: Schema Calculus and Precondition 4.4.3-4
4.5.1-2
lecture 5
September 29, 2009
Z Z: Precondition, Classes and Resources 4.5.3
4.6.1-2
lecture 6
October 6, 2009
Alloy Alloy: Syntax and Analysis
Case study: Library
Supplementary exercises
lecture 7
October 13, 2009
Alloy Alloy: Classes and Traces
Case Study: File System
5.4.1-2
lecture 8
October 20, 2009
Reviewing Model Exam. Model Exam. with Solutions
ZDealer in Alloy
5.4.3
Other remaining exercises
lecture 9
November 10, 2009
Message Sequence Charts MSCs: Basics, Extensions and Consistency 6.2.1-4
Supplementary exercises
lecture 10
November 17, 2009
Message Sequence Charts MSCs: Abstraction, Composition and HMSCs 6.7.1-2, 6.8.1
6.11.1, 6.12.1-4
lecture 11
November 24, 2009
Statecharts UML Sequence Diagrams
Statecharts: Syntax and Well-definedness
7.2.1-3,7.3.1.1
lecture 12
December 1, 2009
Statecharts Statecharts: Semantics 7.3.1.2-4,7.4.1-5
lecture 13
December 8, 2009
Consistency and Modal Logic Hennessy-Milner Logic Hennessy-Milner Logic Exercises
lecture 14
December 15, 2009
Modal Logic Hennessy-Milner Logic + Recursion HML + Recursion Exercises
lecture 15
January 5, 2010
Questions / Solving a model examination Model Exam. with Solutions HML + Regular Exp.
lecture 16
January 12, 2010
No Lecture For those interested, Bas Luttik will give the last instructions at PT 2.23.

Sample Exams:
  1. Partial Exam A d.d. October 1, 2008 and Answers to Partial Exam A d.d. October 1, 2008 (N.B. Exercise 2 (Algebraic Specification) is not treated this year and hence will not be examined.)
  2. Partial Exam B d.d. November 15, 2008
  3. Final Exam d.d. January 15, 2009 and Answers to Exam d.d. January 15, 2009
  4. Re-Exam d.d. June 20, 2009 and Answers to Exam d.d. June 20, 2009



Back to Courses