Text

Course syllabus - Quality assurance - Catching bugs by formal verification

Scope

7.5 credits

Course code

DVA468

Valid from

Autumn semester 2018

Education level

Second cycle

Progressive Specialisation

A1N (Second cycle, has only first-cycle course/s as entry requirements).

Main area(s)

Computer Science

School

School of Innovation, Design and Engineering

Ratified

2018-02-01

Literature lists

Course literature is preliminary up to 8 weeks before course start. Course literature can be valid over several semesters.

    • Ratified date: 2019-06-24
    • Latest update: 2019-06-26

    Reference Literature

    Bérard, Béatrice

    Systems and software verification : model-checking techniques and tools

    Berlin : Springer, cop. 2001 - xii, 190 s.

    ISBN: 3-540-41523-8 (alk. paper) ; LIBRIS-ID: 5368361

    Related to Module 1:

    (optional)

    The book can be ordered from Internet via Akademibokhandeln. Please contact them for more information.

    Ernberg, Patrik; Fredlund, Lars-Åke; Hansson, Hans; Jonsson, Bengt; Orava, Fredrik; Perhson, Björn

    Guidelines for Specification and Verification of Communication Protocol

    URL: Link

    Related to Module 1:

    (optional)

    Clarke, E. M.; Emerson, E. A.; Sistla, A. P.

    Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications

    URL: Link

    Related to Module 1:

    (optional)

    Jonsson, Bengt

    Course Notes for Reactive Systems

    URL: Link

    Related to Module 1:

    (optional)

    Larsen, Kim; Pettersson, Paul; Yi, Wang

    UPPAAL in a Nutshell,

    Springer International Journal of Software Tools for Technology Transfer, 1(1-2), 1997

    URL: Link

    Related to Module 2:

    (otional)

    pages 134-152

    Behrmann, Gerd; David, Alexandre; Larsen, Kim G.

    Tutorial on Uppaal

    In proceedings of the 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM-RT’04). LNCS 3185.,

    URL: Link

    Related to Module 2

    (optional)

Objectives

Software verification focuses on detecting possible bugs in the software prior to its implementation, which is crucial to industry.  The aim of the course is to introduce the students into methods and tools for verifying systems that need to react to external stimuli. The methods use system models with precise formal semantics and will span contract-based verification, model-checking as well as deductive verification. Students will learn some of the theories of formal verification, and how to use tool support in order to verify system models as well as programs.
 
 
 
 
 

Learning outcomes

After completing  the course, the student shall be able to:

1.  describe how formal modelling languages can be applied to model systems
2.  model discrete and real-time systems using finite state automata and timed automata
3.  specify simple system requirements in temporal logics
4.  describe the principles used to verify models in model-checking and deductive verification
5.  describe the principles of contract-based verification of programs
6.  apply tools to model and verify discrete systems and real-time systems
7.  apply contract-based tools to verify software programs (e.g., in C)
 
 
 
 

Course content

The course will cover the following topics: transition systems, modal logics, modeling, verification by model-checking, deductive formal verification, and contract-based verification of programs. Examples of tools that will be used in the course are: UPPAAL, PVS, VCC, Dafny etc.

Tuition

Lectures (web-based).

Specific requirements

120 credits, of which 80 credits in engineering or informatics, including at least 30 credits in computer science or software development. In addition, Swedish course B/Swedish course 3 and English course A/English course 6 are required. For courses given entirely in English, exemption is made from the requirement in Swedish course B/Swedish course 3.
 
 
 

Examination

Written assignment (INL1), 2,5 credits, examines the learning objectives 1 and 2, marks Fail (U) or Pass(G)
Written assignment (INL2), 2,5 credits, examines the learning objectives 3, 4, and 6, marks  Fail (U) or Pass(G)
Written assignment (INL3), 2,5 credits, examines the learning objectives 5 and 7, marks  Fail (U) or  Pass(G)

A student who has a certificate from MDU regarding a disability has the opportunity to submit a request for supportive measures during written examinations or other forms of examination, in accordance with the Rules and Regulations for Examinations at First-cycle and Second-cycle Level at Mälardalen University (2020/1655). It is the examiner who takes decisions on any supportive measures, based on what kind of certificate is issued, and in that case which measures are to be applied.

Suspicions of attempting to deceive in examinations (cheating) are reported to the Vice-Chancellor, in accordance with the Higher Education Ordinance, and are examined by the University’s Disciplinary Board. If the Disciplinary Board considers the student to be guilty of a disciplinary offence, the Board will take a decision on disciplinary action, which will be a warning or suspension.

Study guide

Grade

Two-grade scale

Interim Regulations and Other Regulations

The course completely overlaps towards Formal verification of reactive systems 7,5 credits and Advanced Validation and Verification 7,5 credits