Search course

Use the search function to find more information about the study programmes and courses available at Chalmers. When there is a course homepage, a house symbol is shown that leads to this page.

Graduate courses

Departments' graduate courses for PhD-students.

​​​​
​​

Syllabus for

Academic year
TDA293 - Software engineering using formal methods  
 
Syllabus adopted 2014-02-18 by Head of Programme (or corresponding)
Owner: MPALG
7,5 Credits
Grading: TH - Five, Four, Three, Not passed
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
Block schedule: B

Course module   Credit distribution   Examination dates
Sp1 Sp2 Sp3 Sp4 Summer course No Sp
0110 Laboratory 2,5c Grading: UG   2,5c    
0210 Examination 5,0c Grading: TH   5,0c   30 Oct 2015 pm V   05 Jan 2016 am H

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, MSC PROGR, Year 2 (elective)

Examiner:

Docent  Wolfgang Ahrendt


Replaces

TDA291   Software engineering using formal methods TDA292   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

Skills in object-oriented programing (like Java) are a prerequisite and skills in concurrent programming is an advantage. The course is self-contained, however, a certain maturity in mathematical methods is required, comparable to the admission criteria of the MPALG Masters programme. Alternatively, one of the courses DAT060 Logic in computer science or TDA566 Testing, debugging and verification is a suitable preparation.

Aim

The aim of this course is to introduce students to the two most important styles of formal methods for reasoning about software: automatic and interactive methods. Each style will be introduced using a particular concrete tool for developing software in that style.

Learning outcomes (after completion of the course the student should be able to)

  • judge the potential and limitations of using logic based verification methods for assessing and improving software correctness,
  • judge what can and what cannot be expressed by certain specification/modelling formalisms,
  • judge what can and cannot be analysed with certain logics and proof methods,
  • differentiate between syntax, semantics, and proof methods in connection with logic-based systems for verification.
  • express safety properties of (concurrent) programs in a formal way,
  • describe the basics of verifying safety properties via model checking,
  • use tools which integrate and automate the model checking of safety 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 be represented in a program logic,
  • verify functional properties of simple Java programs with a verification tool,
  • acknowledge the socio-economical costs caused by faulty software,
  • judge and communicate the significance of correctness for software development,
  • approach the issue of correctly functioning software by means of abstraction, modeling, and rigorous reasoning.



Content

Formal Methods is a generic term for system design, analysis, and implementation methods that are described and used with mathematical rigor. The purpose is to construct, with high confidence, systems that behave according to their specification.
The course introduces practically and theoretically the two most important styles of formal methods for reasoning about software: model checking and deductive verification. Each style will be introduced using a concrete tool. On the model checking side, the advantage of an automated method at the same time places restrictions on the kind of properties that can be verified. Accordingly, we concentrate on the verification of safety properties. The lectures cover the following topics:

  • Theoretical foundations of model checking.
  • Property languages and their usage.
  • Performing automated verification with a software model checking tool.


For the deductive verification side, we use KeY, an integrated tool for the formal specification and verification of Java programs. The tool, which is partly developed at Chalmers and University of Gothenburg, supports formal specification in the Java Modeling Language (JML), and translation from JML into logic. An interactive theorem prover is used to formally verify statements about specifications and programs. The lectures cover the following topics:

  • Java Modeling Language (JML)
  • Formal Semantics of Systems
  • Predicate Logic for Specification of Java Programs
  • Translating JML into Dynamic Logic
  • Verifying Proof Obligations

Organisation

There are two lectures each week, introducing formal methods in general, and the technical and theoretical concepts behind the presented methods and tools. Some lectures contain hands-on exercises. The students perform practical case studies using the tools in lab assignments. There is one exercise class per week.

Literature

See separate literature list.

Examination

There are two lab hand-ins that can be done in groups of two. At the end of the course a written exam takes place. To pass the whole course it is necessary to pass both written exam and labs, but they can be passed independently. In case of pass, the grade is determined by the result in the exam.


Page manager Published: Thu 04 Feb 2021.