UE Verification and test theories

Informations aux utilisateurs

Veuillez noter que vous consultez une page du catalogue de formation 2020-2021. Le recrutement est actuellement terminé pour les licences, licences professionnelles, masters, DUT et formations réglementées de santé. Pour consulter le catalogue des formations 2021-2022, cliquez sur le lien suivant.

Diplômes intégrant cet élément pédagogique :


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 makesit 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.

System 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 behaviours (safety properies) or actual proof of well-functioning (progress properties). The aim of this part is to present some basic models and techniques for modelling systems and their properties, and to introduce some corresponding analysis methods for finite state models.

After a short introduction of the general problem and the intinsic difficulty of solving the verification problem, we introduce a basic model for the representation of systems at any level of abstraction. This model is based on transition systems and allows representing systems modularily, with the help of a parallel composition operator. Then, we first consider the verification of safety prperties (the simpler problem) and then the verification of progress properties, starting from some very simple ones. We will also introduce, respectively revise, some basic underlying theories, such as the theory of fixpoint computation.

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 faithfulnesss of the symbolic model with respect to this model.

Program summary :

1/ Theoretical foundations of (software) testing:

  • fault, error, failure.
  • test selection, test execution and test oracle.
  • test levels: unit test, integration test, system test.
  • fault models.
  • test objective, test adequacy.
  • criteria for test adequacy (coverage, regularity, uniformity,...)
  • Test theories and techniques:
  • Automata and transtion system based test
  • Links to other domains (verification, constraint resolution, reliability, …)

2/ System Verification

  • Introduction
  • Transition systems and their composition
  • Theory of fixpoint computation
  • Verification of safety properties
  • Verification of progress properties
  • A logic for expressing properties (LTL)

3/ Verification of cryptographic protocols:

  • Introduction of cryptographic protocols (context, motivation, examples)
  • The symbolic (Dolev-Yao) model : intruder model, protocol verification in bounded scenarios
  • Finding attack by constraint resolution
  • Verification of unbouded protocols using abstraction
  • Application of different automated verification tools dedicated to cryptographic protocols
  • The computational ("real") model and the faithfulness of the symbolic model wrt to this model

Pré-requis recommandés

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

Compétences visées

Students should be aware of the foundations and limits of each approach in order to be able to understand or to define verification requirements for a given application and then to carry out appropriate verification operations.
Two topics (Testing, System Verification, Verification of Cryptographic protocols) will be teached every year.

Informations complémentaires

Lieu(x) : Grenoble
Langue(s) : Anglais