CloseHelpPrint
Kies de Nederlandse taal
Course module: 192140122
192140122
System Validation
Course info
Course module192140122
Credits (ECTS)5
Course typeCourse
Language of instructionEnglish
Contact personprof.dr. M. Huisman
E-mailm.huisman@utwente.nl
Lecturer(s)
Contactperson for the course
prof.dr. M. Huisman
Lecturer
prof.dr. M. Huisman
Academic year2017
Starting block
1A
Application procedureYou apply via OSIRIS Student
Registration using OSIRISYes
Learning goals
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.
Content
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.

Prerequisites
  • 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).
 
Assumed previous knowledge
-
PARTICIPATING STUDY
M-CSC
PARTICIPATING STUDY
M-SC
PARTICIPATING STUDY
M-TEL
PARTICIPATING STUDY
M-EMSYS
Required materials
Handouts
Handout via Union Shop
Recommended materials
Articles
Papers available via Blackboard
Instructional modes
Lecture

Remark
Aanwezigheid bij gastcollegejs is verplicht.
Project unsupervised

Self study without assistance

Tutorial

Tests
Written exam

CloseHelpPrint
Kies de Nederlandse taal