Advanced Validation and Verification 2016

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.

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

- Textbook: Systems and Software Verification. Model-Checking Techniques and Tools. Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci, and Philippe Schnoebelen . (The book can be ordered from internet via Akademibokhandeln. Please contact them for more information.) Reading instructions:

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

- Related to Lecture 1-3

- Guidelines for Specification and Verification of Communication Protocol, Patrik Ernberg, Lars-åke Fredlund, Hans Hansson, Bengt Jonsson, Fredrik Orava, and Björn Perhson.
- Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications Emerson, Clarke & Sistla
- Course Notes for Reactive Systems Bengt Jonsson

- 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.
- Tutorial on Uppaal. Gerd Behrmann, Alexandre David, and Kim G. Larsen. In proceedings of the 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM-RT'04). LNCS 3185.
- Tools:

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

o PVS - Specification and verification system

Other Literature

- Introduction - models and transition systems

- H. Hansson: Time and Probability in Formal Design of Distributed Systems, ISBN 0 444 89940 5, Elsevier, 1994. An extract of relevant sections of the book is available here. [Chapter 1 gives a compact, (hopefully) yet accessible, introduction
- R. Milner: Communication and Concurrency, ISBN 0 13 115007 3, Prentice Hall 1989. [Classical textbook on concurrency theory. Optional reading.] An article presenting a simple related tool: Article presenting the concurrency workbench. Available here. [If you want to play around with models, compositions, equivalences verification etc.]
- B. Jonsson: Course Notes for Reactive Systems. The notes are available here. [Chapter 1 and 2]
- Guidelines for Specification and Verification of Communication Protocols, SICS Perspective Report no. 1, 1991, Available here. [gives an easy to read introduction. You may want to skip some technical details at the introductory reading.]

- Computation Tree Logics (CTL) (intro to modal logics & model checking):

- sections 1.2-1.3 in Hansson (above)
- Chapter 6 in Jonsson (above)
- Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach, Edmund M. Clarke, E. Allen Emerson, A. Prasad Sistla. POPL 1983: 117-126. Also as "Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Trans. Program. Lang. Syst. 8(2): 244-263 (1986)." Available here. [concentrate on sections 1-4]

· 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).