Software Specification (2IW05)

Lectures:
Instruction: There are instructions for four hours per week, on Tuesdays from 15:45-17:30 and Thursdays from 10:45-12:30. There are two groups:
  1. Dr. Pieter Cuijpers, p.j.l.cuijpers@tue.nl and
  2. Dr. Anton Wijs, a.j.wijs@tue.nl .
Practical Project:

The goal of the project is to specify a software system for a web-based "Laptop Shop". The students should register their groups (of three people) in Peach and submit their deliverables (as single .pdf files) using the same system.

The informal project description, deadlines and judgement criteria can be downloaded from here.

The composition of the groups formed so far can be found here. (Last update: 22-11-2011)

Comments on first deliverable can be downloaded from here. (These only include deliverables handed in on paper by December 13 in the morning; comments on the other reports is available via Peach.)

Exams: Final exam (30-01-2012, 14:00-17:00). Material: Chapters 1 - 7 from the course notes (Use-Case and Class Diagrams, Z, Alloy (High-Level) Message Sequence Charts and Statecharts), Chapters 5 and 6 of Reactive Systems book (Modal Logic). No reading material is allowed into the examination.
Material:
Agenda:

date topics slides exercises
lecture 1
November 14, 2011		 Introduction to Software Specification
Use Case Diagrams		 Introduction, Use Cases
lecture 2
November 15, 2011		 Class Diagrams
Case Studies		 Class Diagrams 2.5.1-3
3.3.1-4
lecture 3
November 21, 2011		 Message Sequence Charts Basic MSCs 6.2.1-4
Supplementary exercises
lecture 4
November 22, 2011		 Message Sequence Charts Abstraction and Composition 6.7.1-2, 6.8.1
6.11.1, 6.12.1-4
lecture 5
November 28, 2011		 Z
 Functionality in Z - Part I
Functionality in Z - Part II
 4.2.1-6
4.4.1-2
lecture 6
November 29, 2011		 Z Functionality in Z - Part III 4.4.3-4
4.5.1-2
lecture 7
December 5, 2011		 Alloy Alloy: Introduction
Library Example		 5.4.1-2 (Bring a laptop; install Java and Alloy beforehand)
lecture 8
December 6, 2011		 Alloy Class Diagrams in Alloy
File System Example
Improved Library Example
Alloy Reference Manual 		5.4.4-6
lecture 9
December 12, 2011		 Statecharts Statecharts: Syntax and Micro-Step Semantics 7.2.1-3,7.3.1.1
lecture 10
December 13, 2011		 Statecharts Statecharts: Semantics
Introduction to Modal Logic		 7.3.1.2-4,7.4.1-5
lecture 11
December 19, 2011		 Modal Logic Modal Logic: Semantics and Fixed Points Hennessy-Milner Logic Exercises
lecture 12
December 20, 2011		 Modal Logic Modal Logic: Sets of Equations and Regular Expressions HML + Recursion Exercises
lecture 13
January 9, 2011		 Questions / Solving a model examination Model Examination
Model Examination with Solutions
 HML + Regular Exp.
lecture 14
January 10, 2011		 No Lecture
Sample Exams:
  1. Final Exam d.d. January 30, 2012 and Answers to Final Exam d.d. January 30, 2012
  2. Final Exam d.d. April, 2011
  3. Final Exam d.d. January 26, 2011 and Answers to Final Exam d.d. January 26, 2011
  4. Final Exam d.d. January 15, 2009 and Answers to Exam d.d. January 15, 2009
  5. Re-Exam d.d. June 20, 2009 and Answers to Exam d.d. June 20, 2009
  6. Partial Exam B d.d. November 15, 2008
  7. 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.)


Back to Courses