Syllabus for |
|
| TDA566 - Testing, debugging and verification |
| |
| Syllabus adopted 2013-02-20 by Head of Programme (or corresponding) |
| Owner: TKITE |
|
|
7,5 Credits |
| Grading: TH - Five, Four, Three, Not passed |
| Education cycle: First-cycle |
|
Major subject: Computer Science and Engineering, Information Technology
|
|
Department: 37 - COMPUTER SCIENCE AND ENGINEERING
|
Teaching language: English
Open for exchange students
Block schedule:
A
| Course module |
|
Credit distribution |
|
Examination dates |
|
Sp1 |
Sp2 |
Sp3 |
Sp4 |
Summer course |
No Sp |
| 0108 |
Examination |
7,5 c |
Grading: TH |
|
|
7,5 c
|
|
|
|
|
|
18 Dec 2013 am M, |
23 Apr 2014 pm V |
| 0208 |
Laboratory |
0,0 c |
Grading: UG |
|
|
0,0 c
|
|
|
|
|
|
|
In programs
TIDAL COMPUTER ENGINEERING, Year 3 (compulsory elective)
TKDAT COMPUTER SCIENCE AND ENGINEERING, Year 3 (elective)
TKITE SOFTWARE ENGINEERING, Year 3 (elective)
MPSYS SYSTEMS, CONTROL AND MECHATRONICS, MSC PROGR, Year 1 (elective)
Examiner:
Docent
Wolfgang Ahrendt
Replaces
TDA565
Program verification
Course evaluation:
http://document.chalmers.se/doc/fe2555aa-eb4a-4807-a4c9-3cfbac596537
Go to Course Homepage
Eligibility:
For single subject courses within Chalmers programmes the same eligibility requirements apply, as to the programme(s) that the course is part of.
Course specific prerequisites
The requirement for the course is to have successfully completed one year of an education aiming at a bachelor degree within Computer science or equivalent. Also, basic knowledge of discrete mathematics and object-oriented programming is required.
Aim
The main aim of the course is to provide a basic understanding of techniques that cope with errors in programs. Reoccurring themes are a) the identification of errors, b) their analysis, and c) their removal. The course also provides an understanding of systematic ways of convince oneself that a program unit really does what it should. After the course, students should have understood - and be able to employ - the methods testing (trying to reveal the presence of errors in a systematic way), debugging (the act of isolating and fixing errors), and verification (reasoning about programs in order to guarantee correctness). All these methods only make sence in the the presence of a specification of what the program is supposed to do. In the course students will also learn how to use precise methods for writing requirements.
Learning outcomes (after completion of the course the student should be able to)
* judge the possibilities and limitations of both informal and formal techniques for the discovery, analysis, and resolving of program errors
* understand and express precise specifications of software units
* systematically discover inputs on which a program fails
* locate, analyse, and fix the error which caused the failure
* reason about simple programs for guaranteeing correctness.
Content
Contrasting formal and informal methods, Testing (terminology, coverage, unit tests, JUnit), Debugging (control, workflow, localisation, tools), Formal specifications (assertions, invariants, JML), Automatic test case generation, Formal verification (Hoare logic, tool support). Throughout, the course is concerned with imperative programs in general, and object-oriented programs in particular.
Organisation
The course is held as a combination of lectures, exercise classes and assignments (labs). Details are available from the course home page.
Literature
See the course homepage.
Examination
Written exam, and mandatory hand-ins.