|
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.
Prerequisites
- 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)
|
 |
|