Verification and Validation of Reactive Systems

Instructor

• Reza Pulungan

Schedule

• Lectures
  • Tuesdays: 11:00-11:50, at S2.04
  • Thursdays: 07:00-08:50, at U2.06
• Exams
  • Mid-term:
  • Final:

Objectives

Syllabus

Textbooks

• C. Baier and J.-P. Katoen, Principles of Model Checking, MIT Press, 2008.
• E. M. Clarke Jr., O. Grumberg and D. A. Peled, Model Checking, MIT Press, 1999.
• L. Aceto, A. Ingólfsdóttir, K. G. Larsen, and J. Srba, Reactive Systems: Modelling, Specification and Verification, Cambridge University Press, 2007.

Grading

• Exercise 1: 25%
• Exercise 2: 25%
• Mid-term exam: 25%
• Final exam: 25%

Lectures

Lecture 0 (February 21, 2012)

• Introduction

Lecture 1 (February 23, 2012)

• Introduction and SPIN

Lecture 2 (February 28, 2012)

• SPIN

Lecture 3 (March 1, 2012)

• SPIN + Modelling Parallel Systems

Lecture 4 (March 6, 2012)

• Modelling Parallel Systems

Lecture 5 (March 13, 2012)

• Modelling Parallel Systems

Lecture 6 (March 15, 2012)

• Modelling Parallel Systems

Lecture 7 (March 20, 2012)

• Modelling Parallel Systems

Lecture 8 (March 22, 2012)

• Modelling Parallel Systems

Lecture 9 (March 27, 2012)

• Linear-Time Properties

Lecture 10 (April 3, 2012)

• Linear-Time Properties

Lecture 11 (April 5, 2012)

• Linear-Time Properties

MID-TERM (April 26, 2012)

Lecture 12 (May 1, 2012)

• Linear-Time Properties

Lecture 13 (May 3, 2012)

• Linear-Time Properties

Lecture 14 (May 8, 2012)

• Linear-Time Properties

Lecture 15 (May 10, 2012)

• Linear-Time Properties
• Regular Linear-Time Properties

Lecture 16 (May 22, 2012)

• Regular Linear-Time Properties

Lecture 17 (May 29, 2012)

• Regular Linear-Time Properties

Lecture 18 (May 31, 2012)

• Regular Linear-Time Properties

Lecture 19 (June 5, 2012)

• Regular Linear-Time Properties

Lecture 20 (June 7, 2012)

• UPPAAL

Lecture 21 (June 14, 2012)

• Linear Temporal Logic