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.
Extensive knowledge of first-order logic, basics of program specifications (pre- and postconditions)
Experience with formal analysis techniques.
These prerequisites are covered in the UT bachelor course FMSE (192135201).