| Kursusnavn (dansk): | Softwaretest og verifikation |
| Kursusnavn (engelsk): | Software Test and Verification |
| Semester: | Forår 2005 |
| Udbydes under: | cand.it., internet- og softwareteknologi (int) |
| Omfang i ECTS: | 7,50 |
| Kursussprog: | Engelsk |
| Kursushjemmeside: | https://learnit.itu.dk |
| Min. antal deltagere: | 0 |
| Forventet antal deltagere: | 20 |
| Maks. antal deltagere: | 80 |
| Formelle forudsætninger: | As a prerequisite, students must be able to develop object oriented programs in Java of a size corresponding to roughly 1000 lines of codes.
The prerequisite could have been obtained, for instance, by having followed the course Object Oriented Programming (OOP) at the IT University. Further experience with programming is an advantage but not a prerequisite.
Necessary fundamental concepts from Discrete Mathematics are covered as a part of the course. These concepts include basic constructions on sets, sequences, alphabets and infinite words as well as the proof principles of induction and proof by contradiction. |
| Læringsmål: | The overall goal of the course is 1) to give an understanding of the theoretical underpinnings of Software Test and Verification, 2) to get acquainted with state-of-the-art tools and methods, and 3) to make the participants able to apply the theories and tools in practice.
Errors in software are irritating, costly and potentially dangerous and we all encounter problems coming from software errors. For instance, we frequently need to update software to patch errors and eliminate computer viruses, that are able to spread due to software errors.
In the course we look at various techniques to find errors. These will range from disciplined manual approaches to computer-based automatic and semi-automatic tools. |
| Fagligt indhold: | Having successfully completed the course, the student will be able to:
- Apply the Cleanroom Method for testing and discuss benefits and limitations of code inspection (e.g., as it is used in the Cleanroom Method).
- Perform Unit Testing (e.g., JUnit) on medium-sized programs and discuss benefits and limitations.
- Apply Pre- and Postconditions and Invariants as in Design By Contract to verify minor programs. Explain the theoretical justification for invariants, their benefits and limitations in practical testing.
- Conduct an inductive proof.
- Define Finite Automata, explain the basic construction of determinizing an automaton, and be able to construct a Java program simulating a given automaton.
- Explain the use of automata and Kripke structures for modelling concurrent and sequential programs with the purpose of performing verification.
- Use Temporal logics (CTL and LTL) to express temporal properties of computations.
- Construct models of computations as Finite Automata and Kripke Structures and program them in SMV.
- Apply Symbolic Model Checking for verifying CTL-properties of models of programs within the tool SMV.
- Explain how Symbolic Model Checking can be implemented with Binary Decision Diagrams.
|
| Læringsaktiviteter: | 12 forelæsninger og 12 øvelsesgange Lectures, three smaller mandatory exercises, theoretical and practical exercises.
NB! In the introductory week, meaning from 31 January to 4 February 2005, exercises from 13:00 to 16:00 are cancelled. This means, that there will be only lectures from 9:00 to 12:00. |
| Eksamensform og -beskrivelse: | X. experimental examination form (7-scale; external exam), 13-skala, Ekstern censur At the beginning of the examination, the student draws at random one among the announced questions covering the curriculum.
The student is allowed to write an outline (dk: disposition) on the board based on prepared written notes. After this the student starts to answer the question by himself/herself and is not allowed to further consult written notes or other material. The examination ends with further questions being asked by the examiners in relation to the presentation and the other parts of the curriculum.
The examination takes 30 minutes including evaluation and feedback.
|
| Litteratur udover forskningsartikler: | The books: "Toward Zero-Defect Programming" by Allan M. Stavely, Addison-Wesley, 1999 and "Introduction to the Theory of Computation" by Michael Sipser.
Further articles, online material and notes will be supplied on the course web-page. |
| | |
Kursusoversigt