263-4620-00L  Formal System Development

SemesterAutumn Semester 2011
LecturersT. S. Hoang-Do, F. Klaedtke
Periodicityyearly recurring course
Language of instructionEnglish



Courses

NumberTitleHoursLecturers
263-4620-00 VFormal System Development2 hrs
Fri10:15-12:00CAB G 59 »
T. S. Hoang-Do, F. Klaedtke
263-4620-00 UFormal System Development2 hrs
Fri13:15-15:00CAB G 51 »
T. S. Hoang-Do, F. Klaedtke

Catalogue data

AbstractThe course teaches methods for building correct systems. Participants will learn how to specify system requirements and to incrementally refine specifications to obtain systems that are correct by construction. The course also offers an introduction to the theory and practice of model checking, that is, algorithmic methods of checking whether a system meets its specification.
Objective- Modeling and developing systems using discrete transition systems.
- Reasoning automatically and interactively about systems and proving their correctness.
- Learning basic and advanced methods in system development and system verification.
- Using state-of-the-art tools in formal system development.
ContentAs our daily lives depend increasingly on digital systems, the development of reliable IT systems becomes a concern of overwhelming importance. In this course, participants will learn state-of-the-art methods for building correct systems, which overcome the limitations of simulation and testing. The participants will first learn how to specify system requirements and how to incrementally and interactively refine specifications to obtain systems that are correct by construction. Important principles such as refinement, theorem proving in first-order logic, and set theory will be covered in this part of the course. The second part of the course offers an introduction to the theory and practice of model checking. Model checking concerns the use of methods for automatically verifying whether hardware or software systems meet their specifications. Over the last two decades, model checking has made enormous progress and is nowadays used in large-scale industrial applications. In particular, this part of the course introduces temporal logics, the algorithmic core techniques of model checking, and methods for coping with the state-space explosion problem. Furthermore, the participants will use state-of-the-art tools in the exercises for applying the methods learned in system development.
Lecture notesSlides accompanying each lecture will be distributed.
Literature- Jean-Raymond Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, May 2010.
- Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, 2008.
- Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. The MIT Press, 2000.
Prerequisites / Notice- Previous attendance of the introductory course "Formal Methods and Functional Programming" is a plus.
- Basic knowledge mathematical logic, graph theory, and complexity theory is a plus.
- The participants should have high interests in applying formal modelings and reasoning to practical problems.

Performance assessment

Performance assessment information (valid until the course unit is held again)
Performance assessment as a semester course
ECTS credits5 credits
ExaminersF. Klaedtke, T. S. Hoang-Do
Typeend-of-semester examination
Language of examinationEnglish
RepetitionThe performance assessment is only offered at the end after the course unit. Repetition only possible after re-enrolling.
Admission requirementOnly those who have successfully completed at least 40% of the exercises will be admitted to the examination.
Additional information on mode of examinationOral exam: 30 min.

Learning materials

 
Main linkCourse Homepage
Only public learning materials are listed.

Groups

No information on groups available.

Restrictions

There are no additional restrictions for the registration.

Offered in

ProgrammeSectionType
Computer Science MasterElective Focus CoursesWInformation
Certificate of Advanced Studies in Computer ScienceFocus Courses and ElectivesWInformation