Syllabus for |
|
| TDA294 - Formal Methods in Software Development |
| Formella metoder i mjukvaruutveckling |
| |
| Syllabus adopted 2019-02-21 by Head of Programme (or corresponding) |
| Owner: MPALG |
|
|
7,5 Credits
|
| Grading: TH - Five, Four, Three, Fail |
| Education cycle: Second-cycle |
|
Major subject: Computer Science and Engineering, Information Technology
|
|
Department: 37 - COMPUTER SCIENCE AND ENGINEERING
|
Teaching language: English
Application code: 02125
Open for exchange students: No
Block schedule:
B
| Module |
|
Credit distribution |
|
Examination dates |
|
Sp1 |
Sp2 |
Sp3 |
Sp4 |
Summer course |
No Sp |
| 0117 |
Oral examination |
5,0 c |
Grading: TH |
|
5,0 c
|
|
|
|
|
|
|
|
| 0217 |
Laboratory |
2,5 c |
Grading: UG |
|
2,5 c
|
|
|
|
|
|
|
|
In programs
MPALG COMPUTER SCIENCE - ALGORITHMS, LANGUAGES AND LOGIC, MSC PROGR, Year 1 (compulsory elective)
MPALG COMPUTER SCIENCE - ALGORITHMS, LANGUAGES AND LOGIC, MSC PROGR, Year 2 (elective)
MPSOF SOFTWARE ENGINEERING AND TECHNOLOGY, MSC PROGR, Year 2 (elective)
Examiner:
Wolfgang Ahrendt
Go to Course Homepage
Replaces
TDA291
Software engineering using formal methods TDA292
Software engineering using formal methods TDA293
Software engineering using formal methods
Eligibility:
In order to be eligible for a second cycle course the applicant needs to fulfil the general and specific entry requirements of the programme that owns the course. (If the second cycle course is owned by a first cycle programme, second cycle entry requirements apply.)
Exemption from the eligibility requirement:
Applicants enrolled in a programme at Chalmers where the course is included in the study programme are exempted from fulfilling these requirements.
Course specific prerequisites
The course builds on skills in first-order logic and temporal logic, acquired in DAT060 Logic in Computer Science or in SSY165 Discrete Event Systems. Skills in object-oriented programing (like Java) are also assumed.
Aim
The aim of this course is to teach knowledge and skills in, and judgement about, two important styles of formal methods for reasoning about software: model checking and deductive verification. Each style will be introduced in three ways: conceptual, theoretical, and practical, using a particular tool. The course builds on skills in first-order logic and temporal logic, and shows how these formalisms can be applied, and extended, for the verification of software.
Learning outcomes (after completion of the course the student should be able to)
On successful completion of the course the student will be able to:
Knowledge and understanding- explain the potential and limitations of using logic based verification methods for assessing and improving software correctness
- identify what can and what cannot be expressed by certain specification/modeling formalisms
- identify what can and cannot be analyzed with certain logics and proof methods,
Skills and abilities- express safety and liveness properties of (concurrent) programs in a formal way
- describe the basics of verifying safety and liveness properties via model checking
- successfully employ tools which prove or disprove temporal properties
- write formal specifications of object-oriented system units, using the concepts of method contracts and class invariants
- describe how the connection between programs and formal specifications can berepresented in a program logic
- verify functional properties of simple Java programs with a verification tool.
Judgement and approach- judge and communicate the significance of correctness for software development
- employ abstraction, modelling, and rigorous reasoning when approaching the development of correctly functioning software
Content
The course contains two formal methods for software, model checking and deductive verification.
On the model checking side, we cover the following topics:
- A specification language for concurrent processes
- Verifying assertions
- Synchronization
- Verifying safety and liveness properties in temporal logic
On the deductive verification side, we cover the following topics:
- A unit level specification language for Java programs
- A logic for verification of Java programs
- Verification of Java programs, in the sense that the implementation of a unit fulfils the specification.
Organisation
There are about two lectures each week, and one exercise class per week. The students perform practical case studies using the tools in the laboratory assignments.
Literature
See separate literature list.
Examination including compulsory elements
There are two lab hand-ins that are normally done in groups of two. At the end of the course, there is an oral examination. The lab-hand ins and the oral examination can be passed independently. To pass the whole course, it is necessary to pass both oral examination and the labs. In case of pass, the grade is determined by the result in the oral examination.