Formal Methods in Software Development (WS 2010/11)

Section outline

• Select section General

  Collapse Expand

  General

  Collapse all Expand all

  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.
  

  ---

  • Select activity Questions and Answers

    

    Questions and Answers Forum
• Select section Topic 1

  Collapse Expand

  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.
• Select section Topic 2

  Collapse Expand

  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.
• Select section Topic 3

  Collapse Expand

  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
• Select section Topic 4

  Collapse Expand

  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.
  
  

  • Select activity Exercise 1 (November 8)

    

    Exercise 1 (November 8) Assignment
  • Select activity Exercise 2 (November 15)

    

    Exercise 2 (November 15) Assignment
  • Select activity Exercise 3 (Sztrik, November 22)

    

    Exercise 3 (Sztrik, November 22) Assignment
  • Select activity Exercise 4 (Sztrik, November 29)

    

    Exercise 4 (Sztrik, November 29) Assignment
  • Select activity Exercise 5 (December 6)

    

    Exercise 5 (December 6) Assignment
  • Select activity Exercise 6 (December 13)

    

    Exercise 6 (December 13) Assignment
  • Select activity Exercise 7 (December 20)

    

    Exercise 7 (December 20) Assignment
  • Select activity Exercise 8 (January 17)

    

    Exercise 8 (January 17) Assignment
  • Select activity Exercise 9 (January 24)

    

    Exercise 9 (January 24) Assignment
  • Select activity Exercise 10 (January 31)

    

    Exercise 10 (January 31) Assignment
• Select section Topic 5

  Collapse Expand

  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