Specifikationsmetodik

Specification Methods

Lecturer

Dr. Linas Laibinis

Course description

The goal of this course is to show advantages of using (formal) specifications during program development. We will see how program requirements can be systematically checked/enforced when developing software. We will learn also an industry-strong specification method called B-Method which includes both a specification language and a tool (B-Toolkit). The B-Toolkit tool will be used during exercise sessions.

Time and Place

There will be NO Specifikationsmetodik course this academic year (2006/2007)

Contents and preliminary schedule

 Week
 Time
 Subject
 2
  Mon. 09.01  Introductory lecture.
  Formal software development and formal specifications. (slides)
 2
  Wed. 11.01  Software development using B Method. 
 Introducing abstract machines. (slides)
 3
  Mon. 16.01  Overview of set theory and predicate logic. (slides)
 3
  Wed. 18.01  Semantics of machine operations.  Weakest preconditions.
  Machine consistency conditions. (slides)
 4
  Mon. 23.01  Relations in B specifications.  
  Deferred sets. (slides)
 4
  Wed. 25.01  Functions, sequences, and arrays. (slides)
 5
  Mon. 30.01   !!! No lecture !!!
 5
  Wed. 01.02  Nondeterminism in B specifications. (slides)
 6
  Mon. 06.02  Structuring mechanisms in B. (slides)
 6
  Wed. 08.02  Structuring mechanisms in B (continued). (slides)
 7
  Mon. 13.02  Refining specifications in B. (slides)
 7
  Wed. 15.02  Case study. 
 8
  Mon. 20.02   Summing up. What to expect during the exam?  (slides)

Exercises

Andreas Enbacka is the teaching assistant for the exercise sessions. 

Exam

March 20, 2006 at 12-16 in DC 3102    
April 10, 2006 at 12-16 in DC 3102    

Literature

Schneider. The B Method. An Introduction , Palgrave.

Lano and Haughton. Specification in B: An introduction using the B-Toolkit, Imperial College Press.

Wordsworth. Software Engineering with B, Addison-Wesley.

Linas Laibinis