Search programme

​Use the search function to search amongst programmes at Chalmers. The study programme and the study programme syllabus relating to your studies are generally from the academic year you began your studies.

Syllabus for

Academic year
TDA294 - Formal Methods in Software Development
Formella metoder i mjukvaruutveckling
 
Syllabus adopted 2017-02-20 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
Open for exchange students: No
Block schedule: B

Course elements   Credit distribution   Examination dates
Sp1 Sp2 Sp3 Sp4 Summer course No Sp
0117 Oral examination 5,0c Grading: TH   5,0c    
0217 Laboratory 2,5c Grading: UG   2,5c    

In programs

MPSOF SOFTWARE ENGINEERING AND TECHNOLOGY, MSC PROGR, Year 2 (elective)
MPALG COMPUTER SCIENCE - ALGORITHMS, LANGUAGES AND LOGIC, MSC PROGR, Year 2 (elective)
MPALG COMPUTER SCIENCE - ALGORITHMS, LANGUAGES AND LOGIC, MSC PROGR, Year 1 (compulsory elective)

Examiner:

Wolfgang Ahrendt

Replaces

TDA291   Software engineering using formal methods TDA292   Software engineering using formal methods TDA293   Software engineering using formal methods


  Go to Course Homepage

 

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.


Published: Fri 18 Dec 2009. Modified: Mon 28 Nov 2016