DAT354 Model Checking and Software Verification

Contents and structure

A vast majority of software systems can be characterized as concurrent and distributed software systems in that their operation inherently relies on communication, synchronization, and resource sharing between concurrently executing software components and applications. This development has been accelerated first by the pervasive presence of the Internet as a communication infrastructure, and, in recent years, by, e.g., cloud- and web-based services, networked embedded systems, mobile applications, and multi-core computing architectures. These trends imply that society is increasingly dependent on the reliable and safe operation of software systems. This course concentrates on modelling and property specification languages, algorithms, tools and techniques that enable behavioural modelling and automated verification of concurrent software systems. Examples of industrial applications of software model checking techniques are discussed.

The course covers central paradigms and example languages for modelling parallelism and concurrency, communication, and synchronisation in concurrent systems. Specifically, the course considers Coloured Petri Nets, Promela, and timed automata. Temporal logic is introduced as a language for specification of correctness properties. Algorithms and data structures supporting model checking are covered in conjunction with the central techniques and approaches for tackling the state explosion problem. This includes abstraction, compositionality and behavioural equivalence, memory-efficient storage techniques, on-the-fly verification; counter example generation, partial-order reduction, symmetry reduction, external and distributed model checking, and symbolic model checking. Approaches based on automatically extracting models from source code will also be discussed, as well as the challenges in soundness and precision of software model checkers for C and Java. Novel applications of using temporal specifications during runtime will also be covered.

Learning Outcome

Upon completion of the course the candidate should be able to:

Knowledge

• explain the syntax and semantics of constructs underlying modelling languages for concurrent systems.
• define and explain the syntax and semantics of linear and branching time temporal logic for expressing state- and action oriented correctness properties.
• explain core algorithms, data structures, and paradigms for model checking based on state space exploration.
• discuss and compare approaches for alleviating the state explosion problem in explicit state space exploration.

Skills

• determine proper abstraction level for constructing models of concurrent software.
• formulate correctness criteria for concurrent software using temporal logic.
• apply computer tools for modelling and verification of concurrent software.
• plan and conduct experimental evaluation of software model checking algorithms and their implementation.

General competence

• assess the applicability and limitations of model checking methods for verification of software.
• discuss and relate recent developments and research trends within explicit state software model checking.
• identify central scientific venues and journals within software model checking and verification.

Entry requirements

General admission criteria for the master programme.

Teaching methods

The course consists of a combination of lectures, seminars, and workshops. The lectures will be used for covering the core material of the course. Seminars permit participants to present and discuss recent research papers on topics in model checking and software verification. The seminars will also be used for presentations by visiting researchers in the field. The workshops will be used for experimentation and assessment of tools and technologies supporting model checking and software verification.

Compulsory learning activities

The course includes a number of small assignments concentrating on the application of model checking tools on small and medium sized software systems. A larger project is conducted that focuses on either theoretical developments, design and implementation of model checking algorithms, or a case study applying software model checking tools on a larger example of a concurrent software system. The results from the project must be documented in a final report.

Assessment

The course is graded pass/fail based on the research paper and an oral exam. Each of the two components must result in a pass grade in order to obtain a pass grade for the entire course. Each participant must give one research seminar and a presentation of the larger project. The small assignments must have been approved in order to take the exam.