Kies de Nederlandse taal
Course module: 192140122
System Validation
Course infoSchedule
Course module192140122
Credits (ECTS)5
Course typeCourse
Language of instructionEnglish
Contact persondr. P. van den Bos
Contactperson for the course
dr. P. van den Bos
dr. P. van den Bos
prof.dr. M. Huisman
Academic year2021
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 to 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 to 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 on 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 (2017000117)
Participating study
Master Embedded Systems
Participating study
Master Computer Science
Participating study
Master Internet Science and Technology
Required materials
Recommended materials
Papers available via Canvas
Available via Canvas
Instructional modes

Attendance at guest lectures is mandatory.
Project unsupervised

Self study without assistance


Written exam

Kies de Nederlandse taal