Formal Methods in Software Development (WS 2010/11)

Topic outline

• General
  

  General

  Formal Methods in Software Development (WS 2010/11)
  (KV3/Software Engineering: 326.013, KV4/Computer Mathematics: 326.053)
  

  ---

  Time: Friday 8:30-11:45.
  Room: T 111 (November 10, 10:00-11:45: T 211)
  Start: October 15.
  

  ---

  Important: To take part in the course, you have to enrol in the KUSSS system. The course is offered simultaneously as
  

  • KV3/326.013 (for the master program "Software Engineering") and
    
  • KV4/326.053 (for the master program "Computer Mathematics").

  Please make sure to enrol for the course intended for your degree program.
  

  ---

  This course gives a survey on the use of formal methods for the development of reliable software. More specifically, we deal with

  • specifying sequential programs and concurrent systems,
    
  • computer-supported verification,
  • extended static checking,
  • model checking.

  Furthermore, a guest lecture by Janos Sztrik (University of Debrecen) will give an introduction on
  

  • queueing theory and its application to the performance analysis of computing systems.

  The course consists of two parts:

  1. a lecture part where the fundamental issues of the field are taught, and
  2. an exercise part where practical skills are trained using freely available software tools.

  The grading of the course will be based on a couple of exercises and a final exam.
  

  ---

  Since the exercises will be submitted via Moodle, you also have to login in Moodle and register as a course participant. You will then also receive per email all messages posted in the Announcements forum and may yourself post messages in the Questions and Answers forum.
  

  ---

  • Questions and Answers Forum
• Topic 1
  

  Topic 1

  Schedule
  

  Lectures marked as "KV4" are mandatory for KV4 students but also recommended for KV3 students.
  

  1. October 15: Introduction, the language of logic.
     
  2. October 22: RISC ProofNavigator, Hoare calculus.
     
  3. October 29: Hoare calculus, verification with the RISC ProofNavigator.
     
  4. November 5 (Sztrik): Exponential distribution and its properties, Poisson process, Markov Chains, etc.
     
  5. November 10 (Sztrik, T111+T211): Markov-type Queueing Systems (M/M/1, M/M/n/n, M/M/1//n) and their investigations.
     
  6. November 12 (Sztrik): Modeling tools, Retrial Queueing Systems, Case Studies.
  7. November 19: Hoare calculus, verification with the RISC ProofNavigator.
  8. November 26: JML (part 1), ESC/Java2.
  9. December 3: ESC/Java2, KeY.
  10. December 10: JML (part 2).
      
  11. December 17: modeling concurrent systems, simulating with Spin.
      
  12. January 14: specifying concurrent systems.
      
  13. January 21: model checking concurrent systems with Spin.
  14. January 28: model checking, verifying concurrent systems with the RISC ProofNavigator.
      
  15. February 5: exam.
• Topic 2
  

  Topic 2

  Materials
  

  • Computer Programs/Systems as Subjects of Formal Reasoning
    
  • Introduction (4 on 1)
  • Demonstration Examples
    
  • Fehler im System: der Traum von Software ohne Bugs (restricted)
  • Retrospective: Hoare: An Axiomatic Basis for Computer Programming (restricted)
  • Formal Methods: Practice and Experience (local copy)
    
  • The Language of Logic (4 on 1)
    
  • Specifying and Verifying Sequential Programs
  • Hoare Calculus and Predicate Transformers (4 on 1)
  • An Axiomatic Basis for Computer Programming (restricted)
  • Computer-Supported Program Verification with the RISC ProofNavigator (4 on 1)
  • Demonstration Examples
  • Specifying and Verifying Java Programs
    
  • The Java Modeling Language: Part 1 (4 on 1)
  • Extended Static Checking with ESC/Java2 (4 on 1)
  • Demonstration Examples
    
  • Verifying Java Programs with KeY (4 on 1)
  • Demonstration Examples
  • More Examples
  • The Java Modeling Language: Part 2 (4 on 1)
  • Demonstration Examples
    
  • Proof of Correctness of Data Representations (restricted)
  • Formal Verification of Object-Oriented Software
  • Specifying and Verifying Concurrent Systems
    
  • Modeling Concurrent Systems (4 on 1)
  • Demonstration Examples
  • Specifying Properties of Concurrent Systems (4 on 1)
  • Verifying Concurrent Systems (4 on 1)
  • Demonstration Examples
    
  • Abstrakte Kunst: Fehler finden durch Model Checker (restricted)
  • Talking Model Checking Technology (restricted)
    

  ---

  • Queueing Theory and its Application to the Performance Analysis of Computing Systems (Janos Sztrik)
    
  • Announcement
  • Queueing Theory Books Online
    
  • Java Applets for Queueing Theory
  • List of Queueing Theory Software
    

  ---

  Restricted Area
  

  The password to this area is handed out in class.
• Topic 3
  

  Topic 3

  Software
  

  The following software is used in the course (see the instructions for the use of the course software):
  

  • RISC ProofNavigator
    
  • Java Modeling Language (JML) Tools
  • Use the stable release 5.5 from the archive (not the newer release candidates); also note that the JML tools need an installation of Java 1.4.2.
  • Extended Static Checking for Java (ESC/Java2)
    
  • KeY Verification Environment
    
  • Spin Model Checker
  • Spin Online References
  • Basic Spin Manual
  • Concise Promela Reference
  • Promela Language Reference
• Topic 4
  

  Topic 4

  Exercises
  10 exercises are handed out (two by Prof. Sztrik). From these 10 exercises,
  

  • KV3: the best 7 are used for grading (in total 350 points have to be achieved),
  • KV4: the best 9 are used for grading (at least one must be from Prof. Sztrik; in total 450 points have to be achieved).

  The exercises have to be passed positively to be admitted to the exam.
  
  

  • Exercise 1 (November 8) Assignment
  • Exercise 2 (November 15) Assignment
  • Exercise 3 (Sztrik, November 22) Assignment
  • Exercise 4 (Sztrik, November 29) Assignment
  • Exercise 5 (December 6) Assignment
  • Exercise 6 (December 13) Assignment
  • Exercise 7 (December 20) Assignment
  • Exercise 8 (January 17) Assignment
  • Exercise 9 (January 24) Assignment
  • Exercise 10 (January 31) Assignment
• Topic 5
  

  Topic 5

  Second Exam
  

  A second exam will take place on Thursday, March 31, 17:15-18:45 in BA 9912. You have to register in KUSSS for the exam (lecture number: 326.013) until Monday March 28, 12:00. No materials are allowed, do not forget to bring your student id with you. The exam must be passed positively; it accounts for 50% of the course grade.
  

  • Sample Exam
  • Results
  • Results 2nd Exam