| form | group | time | week | room | teacher | |
|---|---|---|---|---|---|---|
| college | di 9.00-10.45 | 37-44 | MIN-204 | Wishnu Prasetya |
|
|
| do 15.15-17.00 | 37-44 | BBL-071 | ||||
| practicum | groep 1 | di 11.00-12.45 | 38-44 | BBL-106 CLZ | ||
| do 13.15-15.00 | 37-44 | BBL-106 CLZ | ||||
Onderstaande tekst is een oude vakbeschrijving uit collegejaar 2008/2009
|
Most modern software is quite complex. The most widely used approach to verify them is still by conducting ad-hoc testing, which is not a realiable
and scalable way to safeguard against fatal and costly errors. However over the years people have actually invented various clever technologies for validation and verification that go far beyond ad-hoc testing. Exploiting these technologies is the key towards reliable complex software.
This course will introduces you to some of these advanced technologies. In particular we will focus on some fully automatic technologies and on a higher-order based technique.
Model checking is an example of a fully automatic technique that we will discuss. Abstractly, it is a very clever way to explore all possible behavior of a program. So, unlike ordinary testing, model checking guarantees complete coverage! However, model checking only works on finite state programs. We will also discuss test generation, which is also an automated technique ---in particular we will look at techniques to more cleverly generate the test cases (rather than just blindly random them). It is still a testing approach, so it is not as complete as model checking. Still, it is a low-cost approach, which can be a useful complement when model checking cannot be applied. To handle programs with infinite state space we have to turn to a more generic approach called theorem proving. Modern theorem proving tools are usually based on very expressive logics which make them very versatile. Although in principle theorem proving is not an automated approach, modern tools do come with powerful automation libraries. Because of their versatility they potentially have many applications. In addition to discussing techniques we will also show a range of tools implementing the techniques, e.g. HOL, SPIN, FDR, ESC/Java ... The course includes lab sessions and assignments to give you first hand experience with some of those tools. |
On-line documentation and articles
Course outline:
- Hoare logic, specifying Java programs, and automated testing.
- Modelling concurrent systems in Promela and model checking with SPIN
- Symbolic model checking, and model checking in SMV
- Modelling in Higher Order Logic and theorem proving in HOL
- Selected topics in automated software testing