Advanced Validation and Verification 7.5p (DVA442 - online course)
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.
In case you want to take the course, please send a mail to: email@example.com to be added to the list and you will be sent the information on how to connect.
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.
· Prof. Hans Hansson (http://www.es.mdh.se/staff/4-Hans_Hansson): firstname.lastname@example.org
· Lic. Sc. Eduard Paul Enoiu (http://www.es.mdh.se/staff/349-Eduard_Paul_Enoiu): email@example.com
· Assoc. Prof. Cristina Seceleanu (course responsible, firstname.lastname@example.org)
· Dr. Raluca Marinescu: email@example.com
The course will be given as a set of lectures and labs:
[Recorded version of Hans’ first lecture:
(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))
(interactive video version)
· Lecture 3: (Sept. 30) Hans (included in slides for Lecture1)
· Lab 2 (Oct. 17): UPPAAL lab 1 (Raluca) (description)
· 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.
Laboratory work (3.5p) and exam (4.0p).
Here are some sample exam questions related to L1-L3.
At least 120 university course points or corresponding, out of which at least 60 should be from computer science, computer engineering or corresponding subjects.
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.
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
· 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).