Course syllabus for Formal Methods in Software Development

Course syllabus adopted 2021-02-26 by Head of Programme (or corresponding).

Overview

  • Swedish nameFormella metoder i mjukvaruutveckling
  • CodeTDA294
  • Credits7.5 Credits
  • OwnerMPALG
  • Education cycleSecond-cycle
  • Main field of studyComputer Science and Engineering, Software Engineering
  • DepartmentCOMPUTER SCIENCE AND ENGINEERING
  • GradingTH - Pass with distinction (5), Pass with credit (4), Pass (3), Fail

Course round 1

  • Teaching language English
  • Application code 02134
  • Block schedule
  • Open for exchange studentsYes

Credit distribution

0117 Oral examination 5 c
Grading: TH		5 c
0217 Laboratory 2.5 c
Grading: UG		2.5 c

In programmes

Examiner

Go to coursepage (Opens in new tab)

Eligibility

General entry requirements for Master's level (second cycle)
Applicants enrolled in a programme at Chalmers where the course is included in the study programme are exempted from fulfilling the requirements above.

Specific entry requirements

English 6 (or by other approved means with the equivalent proficiency level)
Applicants enrolled in a programme at Chalmers where the course is included in the study programme are exempted from fulfilling the requirements above.

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.

The course examiner may assess individual students in other ways than what is stated above if there are special reasons for doing so, for example if a student has a decision from Chalmers on educational support due to disability.