Aller au menu Aller au contenu
Une voie, plusieurs choix
Informatique et Mathématiques appliquées
Une voie, plusieurs choix

> Formation > Cursus ingénieur

Verification and test theories - WMM9MO04

A+Augmenter la taille du texteA-Réduire la taille du texteImprimer le documentEnvoyer cette page par mail Partagez cet article Facebook Twitter Linked In Google+ Viadeo
  • Volumes horaires

    • CM : 18.0
    Crédits ECTS : 3.0

Objectifs

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.

Contact Ioannis PARISSIS, Cristian ENE, Susanne GRAF

Contenu

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:
    1. Fault, error, failure.
    2. Test selection, test execution and test oracle.
    3. Test levels: unit test, integration test, system test.
    4. Fault models.
    5. Test objective, test adequacy.
    6. Criteria for test adequacy (coverage, regularity, uniformity,...)
    7. Test theories and techniques:
    8. Automata and transtion system based test
    9. Links to other domains (verification, constraint resolution, reliability, …)
  2. System Verification
    1. Introduction
    2. Transition systems and their composition
    3. Theory of fixpoint computation
    4. Verification of safety properties
    5. Verification of progress properties
    6. A logic for expressing properties (LTL)
  3. Verification of cryptographic protocols:
    1. Introduction to cryptographic protocols (context, motivation, examples)
    2. The symbolic (Dolev-Yao) model: intruder model, protocol verification in bounded scenarios.
    3. Finding attacks by constraint resolution.
    4. Verification of unbounded protocols using abstraction.
    5. Application of different automated verification tools dedicated to cryptographic protocols.
    6. The computational ("real") model and the faithfulnesss of the symbolic model wrt to this model.


Prérequis

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

Contrôles des connaissances

Semestre 9 - L'examen existe uniquement en anglais 



Informations complémentaires

Semestre 9 - Le cours est donné uniquement en anglais EN

Cursus ingénieur->Master 2 Informatique->Semestre 9

A+Augmenter la taille du texteA-Réduire la taille du texteImprimer le documentEnvoyer cette page par mail Partagez cet article Facebook Twitter Linked In Google+ Viadeo

mise à jour le 15 janvier 2017

Grenoble INP Institut d'ingénierie Univ. Grenoble Alpes