Formal Methods in Software Development

Jump to today

Course-PM

TDA294 / DIT271 Formal Methods in Software Development lp1 HT19 (7.5 hp)

Course is offered by the department of Computer Science and Engineering

Contact details

The teaching team of this course consists of:

The course assistants Andreas (room 5461, EDIT building) and Oskar (room 5453, EDIT building) offer office hours on request to help you with questions. You can make an appointment with one of them by email. It is not very likely that they are available if you just drop in.

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

TimeEdit

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, there is highly relevant material in the book Deductive Software Verification - The KeY Book, co-edited by the course teacher (accessible from within the Chalmers network). 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 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, 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:

  • Java Modeling Language (JML)
  • Formal Semantics of Systems
  • Predicate Logic for Specification of Java Programs
  • 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

This year, we use Canvas for the first time. However, we stick to the Fire system for lab hand-ins.

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 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

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 an update to 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