Module "Vérification et Test de Systèmes Embarqués" (VTES)
ESIR 3 2011-2012
Head: Sophie Pinchinat
Teachers: Thierry Jéron (CM), Sophie Pinchinat (CM), Loig Jézéquel (TD)
Pre-requisites: propositional logic, graph and automata
theories and algorithms, basic notions of computational complexity.
Synopsis
La conception de systèmes logiciels repose désormais sur l’assemblage
complexe de composants interactifs, qui communiquent et partagent des
ressources afin d’assurer un service ; leur utilisation dans des
systèmes critiques et sûrs requiert l’emploi systématique de méthodes
de modélisation, de vérification et de test en réponse aux exigences
fonctionnelles (services attendus, fonctionnalités et autres aspects
indépendants de l’implémentation) et aux exigences non-fonctionnelles
(performance en temps et en consommation, contraintes
d’exécution, mémoire, taille, poids, et robustesse aux fautes,
accessibilité aux ressources, résistance aux défaillances ou aux
attaques, etc.), sachant que les sources principales de complexité sont
la concurrence, le temps-réel et l’incertitude.
La vérification formelle repose sur la modélisation formelle (des
aspects pertinents du système et des propriétés attendues) suivi d’une
analyse algorithmique. L’interaction coopérative/compétitive entre
composants (tel qu’un système et son environnement de test) se modélise
par un jeu à plusieurs joueurs. Pour l’aspect temps-réel, on combine
des transitions d’états discrètes avec des évolutions continues. Pour
l’incertitude due à l’environnement, on utilise des changements d’états
probabilisés.
Le test, bien qu’étant la technique la plus utilisée pour valider la
qualité des systèmes, est souvent un processus ad hoc. Il existe
toutefois une méthodologie formelle s’appuyant sur des modèles et des
théories bien fondées, dont on dérive des méthodes (partiellement)
automatisées, par techniques d’analyse et de synthèse (par exécution
symbolique, résolution de contraintes, et vérification formelle). C’est
ce que recouvre le terme « test basé sur les modèles » dans la
littérature consacrée.
La première partie du cours équipe les étudiants des notions
fondamentales de modélisation formelle et d’analyse algorithmique s’y
afférant, en développant leurs capacités à utiliser/concevoir des
formalismes adéquats ; elle leur procure le discernement nécessaire
pour convertir le cadre formel utilisé en méthodes effectives.
La deuxième partie du cours est centrée sur le test de conformité.
Après une introduction à cette notion, nous étudions la théorie du test
et la génération automatique de tests pour deux modèles. Dans une
première partie nous considérons des modèles simples de systèmes
réactifs à entrée/sorties, les IOLTS, la théorie du test sous-jacente
basée sur la relation de conformité ioco, et la génération de tests
dans ce contexte. Dans la deuxième partie, nous considérons des modèles
temporisés entrées/sorties (TAIO), étudions la théorie du test
sous-jacente basée sur la relation de conformité tioco, et les
problèmes plus complexes de génération de tests qui en découlent.
Pré-requis
Logique propositionnelle, théorie et algorithmique des automates et des
graphes, notions de bases en calculabilité et complexité.
Mots-clé
Modèles opérationnels, systèmes modulaires, systèmes hybid, systèmes
temporisés, automates, logiques, jeux infinis, systèmes à base de
composants, interface, vérification, test, graphes de flot de contrôle,
couverture, oracle.
Description détaillée du cours
Partie 1: Fondements de la modélisation formelle et de la vérification (12 h)
- Modèles (2h): systèmes hybrides et temporisés,
modules, modèles d’exécution (synchrones, asynchrones, «
time-triggered », etc.)
- Problèmes de vérification des automates temporisés
(4h): régions, analyse d’accessibilité, bisimulation, problèmes
indécidables;
- La trilogie « Automates, Logique et Jeux Infinis » (6h).
Partie 2: Test Formel (4 h)
- Test de conformité de systèmes interactifs (4h):
Modèles et théorie du test de conformité; Sélection de test par les
techniques de vérification.
Bibliographie
- C. Baier and J.-P. Katoen. Principles
of Model-checking. MIT Press, 2009.
- Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A.
Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph
Sifakis, Sergio Yovine: The Algorithmic Analysis of Hybrid Systems.
Theor. Comput. Sci. 138(1): 3-34 (1995).
- Automata, logics, and infinite
games: A guide to current research. Eds : Grädel E., Thomas W.,
Wilke T., outcome of a Dagstuhl seminar, February 2001, Springer, ISBN
3-540-00388-6, 2002.
- J. Tretmans. Test generation
with inputs, outputs and repetitive quiescence. Software -
Concepts and Tools, 3:103-120, 1996.
- N. Bertrand, T. Jéron, A. Stainer, M. Krichen. Off-line Test Selection with Test Purposes
for Non-Deterministic Timed Automata. In 17th International
Conference on Tools and Algorithms for the Construction And Analysis of
Systems (TACAS), LNCS, Volume 6605, Pages 96-111, Saarbrücken,
Germany, April 2011.
Support de cours
Forthcoming slides on timed-automata (by Sophie Pinchinat)
Forthcoming slides on
Automata, Logic and Games (by Sophie Pinchinat)
Forthcoming slides on
Model-based Conformance Testing (by Thierry Jéron)
Assessments (2)