Course syllabus

Jump to today

This iteration of the course will start in online mode. We may have on-campus activities as we go along. Those will be announced in due time.

Course-PM

TDA294 / DIT272 Formal Methods in Software Development lp1 HT21 (7.5 hp)

Course is offered by the department of Computer Science and Engineering

Contact details

The teaching team of this course consists of:

Oskar offers online meetings on request to help you with questions. You can make an appointment with him by email.

Course purpose

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.

Schedule

Overview of Lectures and Exercises, with corresponding material (telling also whether the event is via Zoom, otherwise the physical location)

For lectures and exercises which are online, information on how to join them will be published consecutively under the "Zoom" link in the course navigation. To join a Zoom meeting, you have to be signed in into Zoom via your institutional domain (for instance, by signing in using the "Sign In with SSO" option, choosing chalmers.zoom.us or gu-se.zoom.us, respectively). Note that the starting time of the Zoom meeting is earlier than the starting time of the lecture. The first 15 min are drop-in time.

Course literature

The course does not have mandatory literature. However, the following literature can support very well the learning:

For the first part we partly use the book Principles of the Spin Model Checker, mostly Chapters 1-5. The book is available as E-book from within the Chalmers network. Some additional material for that book, in particular the examples, can be found online. In particular, you find there a few pages "Supplementary material on version 6 of Spin", which corrects some outdated information from the main book.

For the second part, you find related material in the book Deductive Software Verification - The KeY Book, co-edited by the course teacher (accessible from within the Chalmers network). That book goes a lot deeper than this course. Yet, there is very relevant material in selected chapters. Chapter 1 in the book introduces general principles of deductive software verification in general, and of the KeY approach in particular. Chapter 7, co-authored by the course teacher, is a tutorial on formal specification of Java applications using the Java Modeling Language. Chapter 16 is a tutorial for the overall verification process using the KeY approach and tool. Chapter 15, co-authored by the course teacher, is a tutorial on using the the KeY prover.

Additional literature

Model checking:

Logic:

  • There are many good books on first-order logic. We recommend, as a good introduction, Logic in Computer Science by Michael Huth and Mark Ryan. (Note who is mentioned in the acknowledgements for the second edition.)
  • First-order logic with Java-style types as discussed in the second part of the course is described in depth in Chapter 2 of Deductive Software Verification - The KeY Book.

JML:

Course design

Formal Methods is a generic term for system design, analysis, and implementation methods that are described and used with mathematical rigour. 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, we use the model checker SPIN. The advantage of an automated method at the same time places restrictions on the kind of properties that can be verified. 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 Gothenburg University, 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:

  • First-Order Logic as a foundation for specification and verification
  • Java Modeling Language (JML)
  • Translating JML into Dynamic Logic
  • Verifying proof obligations

In addition to the lectures, the course has 6 exercise sessions, which are highly recommended. The questions and tasks which will be discussed in either exercise session are published beforehand. Students should familiarise themselves with the questions before the exercise session.

The course has two mandatory lab hand-ins, one about model checking, and one about deductive verification. Each submission of a lab is either rejected (meaning you must improve it) or accepted (meaning you have passed the lab). If the first submission is rejected you have ca. one week to resubmit a corrected version. It is a requirement to do the labs in pairs.

Changes made since the last occasion

While the course is constantly being improved, there are no major changes this year. However, there is a change in the grading scale for the Gothenburg University students. Since this year, the Gothenburg University students have the same grading scale as the Chalmers students, U-3-4-5 (instead of U-G-VG as in earlier instances of the course).

Learning objectives and syllabus

Learning objectives:

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 analysed 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 be represented 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

This is a joint course of Chalmers and the University of Gothenburg. Accordingly, it has two course plans:

Examination form

In addition to the two obligatory lab hand-in assignments, the course is examined via individual, oral examination of 30 min per student. During the 30 minutes, numerous selected topics from the course will be discussed. Frequent context switch is therefore inevitable and should be expected.

Questions by the teacher will be of varying nature, ranging from very concrete questions where the expected answer is a concrete solution (or some steps of a concrete solution, until we switch context), to questions where the expected answer shows high level understanding. In all cases, the teacher will help the student to meet the expected level of detail in the answer.

Please observe the learning outcomes of the course as outlined in the course plan.

In general, all topics that were discussed in the lectures and exercises can be subject to questions in the examination. There are a few restrictions, however. Those are described below. Questions related to the lab assignment are also possible, but will not be the focus.

Topics that are excluded from the exam:

  • Decidability, closure properties
  • Object creation in dynamic logic

Topics where only basic understanding is expected, rather than details:

  • Semantics of first-order logic and dynamic logic, and updates
  • Systematic construction of a (generalised) Büchi automaton that corresponds to a given LTL formula, following the algorithm presented in the lecture
  • Syntax of KeY input files
  • Computing the effect of updates on formulas and terms
  • The heap model in dynamic logic
  • Translation of JML to dynamic logic (incl. normalisation of JML)
  • Handling of method calls in the sequent calculus for dynamic logic

Course summary:

Date Details Due