Text

Course syllabus - Advanced Validation and Verification

Scope

7.5 credits

Course code

DVA442

Valid from

Autumn semester 2015

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

2015-02-02

Status

This syllabus is not current and will not be given any more

Literature lists

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

    • Ratified date: 2015-08-10
    • Latest update: 2015-09-25

    Books

    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

Objectives

 
Software verification and validation focus on detecting possible bugs in the software prior to its implementation, which is crucial to industry. The aim of the course is to give in-depth knowledge in some of the theories underlying software modeling and exhaustive verification by means of formal techniques. Students will learn about the state-of-the-art research and tools in formal verification of discrete and real-time systems.
 
 
 
 

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 and 
5. apply tools to model and verify discrete systems and real-time systems.

Course content

The course will cover the following topics: transition systems, modal logics, modeling, verification by modelchecking,
and deductive formal verification. The tools UPPAAL and PVS (or equivalent) will be used.

Tuition

Lectures and laboratory assignments.

Specific requirements

At least 120 ECTS credits or corresponding, out of which at least 60 should be from computer science. Discrete mathematics 7,5 credits.

Further requirements are Swedish B/Swedish 3 and English A/English 6. If the course is given in English, there is no reguirement for Swedish 3.

 

Examination

Laboratory work (LAB1), 3,5 credits, (examines the learning outcomes 3 and 5), marks Fail (U) or Pass (G)
Examination (TEN1), 4 hp, written examination, (examines the learning outcomes 1-4), marks Fail (U), 3, 4 or 5

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.

Grade

Pass with distinction, Pass with credit, Pass, Fail

Interim Regulations and Other Regulations

The course complety overlaps with Advanced Software Verification and Validation 7,5 credits.