Kies de Nederlandse taal
Course module: 192140122
System Validation
Course info
Course module192140122
Credits (ECTS)5
Course typeStudy Unit
Language of instructionEnglish
Contact personprof.dr. M. Huisman
Contactperson for the course
prof.dr. M. Huisman
prof.dr. M. Huisman
Academic year2023
Starting block
Application procedureYou apply via OSIRIS Student
Registration using OSIRISYes
To learn how to apply formal techniques and tools to find bugs in software designs and systems. After the course, the student will be able to:
  • Describe the essential characteristics of the main formal techniques, and describe in what situation what kind of tool is most appropriate.
  • Gather informal plain text requirements and transform these into a set of formal requirements.
  • Write formal specifications in different specification formalisms, and choose the most appropriate formalism to write a specification.
  • Apply abstraction techniques to hide implementation details
  • Predict what will happen when a validation tool is applied to a model or code fragment.
  • Interpret the meaning of error messages produced by different validation tools.
  • Complete and correct specifications, so that a validation tool will not report errors in the specification anymore.
The complexity of software and hardware systems is rapidly increasing and so is their vulnerability with respect to errors. The course System Validation focuses on validation techniques and methods to assess the correctness and reliability of information- and communication technology systems. Several validation tools will be presented to illustrate the broad application range of formal methods and techniques. All tools will be studied from a user perspective, i.e., the focus is not on how the techniques and tools are implemented, but on how they can be used efficiently to increase the quality of software.

Besides understanding how the different tools and techniques can be used, a user also needs to understand how to "communicate" with them, i.e., how to express what is the expected behaviour of an application. Various formal specification techniques will be presented, and special attention will be given to the transition from informal specification to formal specification. Also, we will discuss which techniques are most suited to verify particular classes of properties.

In addition to regular lectures, several guest lecturers will be invited to illustrate how system development can go wrong in practice, and how validation can be used to improve the quality of system development.

This is a hands-on course: in several practical assignments, the students will learn how to use the tools and techniques. After the course they will know when and how to use these validation tools.

The acquired skills will be assessed in a written open book examination. The assignments and exam together will determine the final grade.

  • Basic knowledge of first-order logic, basics of program specifications (pre- and postconditions)
These prerequisites are covered as part of the UT bachelor course Software Systems (202001023)
Participating study
Master Embedded Systems
Participating study
Master Computer Science
Required materials
Concise Guide to Software Verification - From Model Checking to Annotation Checking, Huisman M and Wijs A, Springer 2023, ISBN 978-3-031-30169-8, e-book 978-3-031-30167-4
Recommended materials
Papers will be provided via Canvas
Instructional modes

Attendance at guest lectures is mandatory.
Project unsupervised

Self study without assistance


Assignments, Written exam

Kies de Nederlandse taal