Advanced Validation and Verification 7.5p (DVA442 - online course)

Autumn 2016

 

Lecturers: Prof Hans Hansson, Ph.D. student Eduard Paul Enoiu, Assoc. Prof. Cristina Seceleanu (course responsible)

Lab assistant: Raluca Marinescu, Ph.D.

 

Mälardalen Real-Time Research Centre (MRTC), Mälardalen University (MDH), Sweden.

www.mdh.se

 

In case you want to take the course, please send a mail to: cristina.seceleanu@mdh.se to be added to the list and you will be sent the information on how to connect.

Course description

The theme of the course is formal modeling and verification techniques for concurrent discrete and real-time systems. The course will cover the following topics: transition systems, modal logics, modeling, verification by model-checking, and deductive formal verification.

 

The main goal of the course is to give students the basics and some hands-on experience on creating abstract models of systems (be they communication protocols or any type of reactive system) and using verification techniques that are able to check the models exhaustively (for all possible behaviors) prior to implementation, in order to spot possible bugs at an early stage of design. The methods are called formal as they rely on rigorous underlying theories.

The course will be given as a set of online lectures and lab sessions, via Adobe Connect.

Lecturers

·         Prof. Hans Hansson (http://www.es.mdh.se/staff/4-Hans_Hansson): hans.hansson@mdh.se

·         Lic. Sc. Eduard Paul Enoiu (http://www.es.mdh.se/staff/349-Eduard_Paul_Enoiu): eduard.paul.enoiu@mdh.se

·         Assoc. Prof. Cristina Seceleanu (course responsible, cristina.seceleanu@mdh.se)

(http://www.es.mdh.se/staff/173-Cristina_Seceleanu)

 

Lab assistant:

·         Dr. Raluca Marinescu: raluca.marinescu@mdh.se

(http://www.es.mdh.se/staff/350-Raluca_Marinescu) 

Lectures

The course will be given as a set of lectures and labs:

 

· Lecture 1: (Sept. 16) Introduction, modeling untimed systems, transition systems (Cristina+Hans) (Course information, slides for Lecture1-Lecture3)

        [Recorded version of Hans’ first lecture:

http://www.hapyak.com/portal/viewer/471a95d110b6370dbb9ab9f0d23930be 

(interactive video version; should be ok now)

https://dl.dropboxusercontent.com/u/9920646/VoV-Lecture-1%28HansH%29.m4v (best quality version)

https://vimeo.com/182739115 (slightly lesser quality)]

· Lecture 2: (Sept. 23) Modal logics, verification (Hans) (included in slides for Lecture1)

[(explanations and illustration of observation equivalence (using the 1 and 2 buffer example))
https://dl.dropboxusercontent.com/u/9920646/Observation%20equivalence%20example.m4v 

(interactive video version)
http://www.hapyak.com/portal/viewer/aba5cc5ff32eea0a5be42ab8e355d5a1]

· Lecture 3: (Sept. 30) Hans (included in slides for Lecture1)

[recorded video https://vimeo.com/184700141?utm_source=email&utm_medium=vimeo-cliptranscode-201504&utm_campaign=28749 ]

· Lab 1: (Oct. 3) Untimed systems lab (Raluca) (description, solutions)

· Lecture 4: (Oct. 5) Modeling timed system, timed automata, TCTL, real-time testing (Eduard) (slides, video)

· Lecture: 5: (Oct. 14) Timed automata syntax of UPPAAL, Model-checking with regions (Eduard) (slides 1st hour, slides 2nd hour)

· Lab 2 (Oct. 17): UPPAAL lab 1 (Raluca) (description)

· Lecture 6: (Oct. 19) Symbolic model-checking: reachability analysis with clock constraints (Eduard) (slides) (video)

· Lecture 7: (Oct. 21) Introduction to propositional, predicate, and higher order logics (Cristina) (slides, material1, material2 - the recording of the lecture will be added later)

· Lab 3: (Oct. 24) UPPAAL lab 2 (Raluca) (description)

· Lecture 8: (Oct. 26) Deductive formal verification techniques for reactive systems (Cristina) (slides)

· Lecture 9: (Oct. 27) More on deductive formal verification techniques and PVS (Cristina) (slides)

· Lecture 10: (Oct. 28) Extra time slot. May not be used.  

· Exam: (Nov. 4)

· Re-exam (Jan 13, 2017, June 9, 2017)

 

The detailed schedule is available here Schema för DVA442.

Examination

Laboratory work (3.5p) and exam (4.0p).

Here are some sample exam questions related to L1-L3.

Prerequisites

At least 120 university course points or corresponding, out of which at least 60 should be from computer science, computer engineering or corresponding subjects.

 

Laboratory assignments

1.    Modeling and verification of an untimed concurrent system - lab instructions

2.   Modeling and verification of a timed system (timed systems + TCTL) - lab instructions

 

Lab reports for labs 2, and 3 should be handed in no later than two weeks after the scheduled lab. Assignments should be submitted via e-mail to Raluca.

 

Course Material

o    Chapter 1 - Introduction: 1.1-1.7

o    Chapter 2 - Temporal logic: 2.1-2.5

o    Chapter 3 - Model checking: 3.1, 3.3

o    Chapter 4 - Symbolic model-checking: 4.1 (skip 4.2-4.4)

o    Chapter 5 - Timed automata: 5.1-5.5

o    Chapter 6 - Reachability properties: 6.1-6.3

o    Chapter 7 - Safety properties: 7.1-7.3 (skip 7.4)

o    Chpater 8 - Liveness properties: 8.1-8.2, 8.5 (skip 8.3-8.4)

o    Chapter 9 - Deadlock-freeness: 9.1-9.2 (skip 9.3)

o    Chapter 13 - SPIN: 13.1-13.6

o    Chapter 15 - UPPAAL: 15.1-15.6

o    UPPAAL - Tool environment for modelling and verification of timed systems

o    PVS - Specification and verification system

Other Literature

· Timed Systems (Timed Automata, TCTL):

o    A Theory of Timed Automata, Rajeev Alur and David L. Dill. Theoretical Computer Science, vol 126, number 2, pages 183-235. 1994.

o    UPPAAL in a Nutshell, by Kim Larsen, Paul Pettersson and Wang Yi. Springer International Journal of Software Tools for Technology Transfer, 1(1-2), December 1997, pages 134-152.

o    Timed Automata - Semantics, Algorithms and Tools, Johan Bengtsson and Wang Yi. Tutorial on timed automata (a book chapter in Rozenberg et al, 2004, LNCS).