Verification and test theories - WMM9MO04

Objectif(s)

Students should be aware of the foundations and limits of each approach in order to be able to understand or to define testing and verification requirements for a given application and then to carry out appropriate testing and verification strategies.

Every 2 of the 3 following topics will be addressed:
1) Testing theories
2) general verification theory
3) verification of crypto-protocols

in 2019/20, topics 1 and 2 will be tought

Contenu(s)

Basics:
Labelled transition systems (LTS) as models of components, programs, systems and their specifications.
Notions of (parallel) composition. Notions of refinement and equivalence for comparing programs and specifications to be able to express assertions like "program P satisfies property Phi", "program P implements specification S", "programs P1 and P2 are equivalent" ...
Predicate transformers and fixpoint theory as a basis for expressing and solving these validation problems
The techniques presented in this course will be applied to examples using the Uppaal (http://uppaal.org) and CADP (http://cadp.inria.fr) tools.

Testing.
Test is the most common verification method applied in industrial development projects. To meaningfully apply testing techniques, knowledge on its foundations and restrictions is essential.
A first objective of this course is to explain the basic notions and the theoretical foundations of (software) testing. These basic notations are, for instance, defined on labelled transition systems and Mealy automata.
A second aim of this course is to show that the existence of a formal framework makes it possible to automate to a large extent test case generation, test execution and test evaluation. We present approaches for which tools exist implementing model-based testing. We present a tool for automatic test case generation

Verification.
In the case of certain critical functionalities or systems, it is desirable to go beyond testing in order to be able to actually guarantee some critical properties: absence of bad behaviors (safety properties) or actual proof of well-functioning (progress properties).
We introduce some ways for expressing properties and corresponding analysis methods for finite state models.

Verification of cryptographic protocols.
Nowadays secured applications are present everywhere : e-banking, mobile phone, electronic voting, secured web site ... All these applications use cryptographic protocols. These protocols assure the confidentiality and integrity of exchanged messages but offer also some other functionalities : authentication, fairness, privacy ... The aim of this part is to provide some theoretical foundations and to illustrate some techniques used to design and analyze security protocols.
After a short introduction to cryptography in general, and cryptographic protocols in particular, we present the symbolic (Dolev-Yao) model. Throughout examples, we give the theoretical foundations of cryptographic verification. During one lab session, we apply existing tools for illustrating the studied methods on some examples. Students will by them-self prove secure or find some flaws using automatic tools. Then, we take a look to the computational model and the faithfulness of the symbolic model with respect to this model.

A basic software engineering course, basic notions of mathematics, logic and of automata theory (some knowledge on models for concurrency and model-checking techniques would be a plus).