ATF

Imprimer

ATF : Analyse et Test Formels de modèles

Responsable : Philippe Dhaussy (mail)

Équipe pédagogique : Philippe Dhaussy, Frank Singhoff, Valérie-Anne Nicolas (mail)

Description

Depuis une vingtaine d'année, de nombreuses avancées ont contribué à l'amélioration des techniques de modélisation des systèmes critiques à prédominance logicielle. Dans un souci de recherche de fiabilité de plus en plus grande des Systèmes Temps Réel Embarqués critiques (STRE), la mise au point des composants logiciels implique la nécessité de renforcer les activités d’analyse durant les phases amont du cycle de vie, ceci afin de réduire l’effort de test. La capacité des modèles logiciels de conception à être exploités lors des analyses formelles devient alors incontournable.

Les méthodes formelles deviennent un domaine important du génie logiciel. Elles définissent des techniques de spécification et d’analyse des systèmes qui se positionnent de manière complémentaire à la simulation et au test. Le module ATF sera dédié à la présentation, d’une part, de techniques d’analyse d’ordonnancement et d’analyse fonctionnelle de modèles. D’autre part, le module introduit des techniques de test formel et plus particulièrement le test basé sur des modèles ou « Model-Based Testing ».

Pour le premier type d’analyse, la théorie de l'ordonnancement temps réel propose des méthodes algébriques et algorithmiques afin de prédire le comportement d'un système temps réel. Cette théorie a donné lieu à de très nombreuses recherches et des résultats théoriques qui permettant de prédire le comportement temporel de systèmes temps réel monoprocesseur composés de tâches périodiques. La théorie de l'ordonnancement temps réel propose des algorithmes d'ordonnancement et des méthodes analytiques (appelées tests de faisabilité) qui permettent au concepteur de vérifier a priori le comportement temporel de son système.

Les analyses fonctionnelles sont abordées au travers des techniques dites de « vérification de modèles » ou « model-checking ». Celles-ci impliquent de disposer de modèles conçus sous la forme d’un réseau d’automates communicants. La vérification d’un modèle consiste en la démonstration de véracité de propriétés sur le comportement de ce modèle. Les exigences à vérifier sur ces modèles sont formalisées sous la forme de propriétés écrites avec des langages de logiques temporelles (LTL, CTL).

Le test logiciel regroupe un ensemble de techniques, statiques ou dynamiques, permettant d’évaluer et d’améliorer la qualité d’un logiciel à travers des propriétés fonctionnelles (sûreté) ou non-fonctionnelles (test de charge, sécurité…). La pratique du test est de moins en moins empirique grâce à des travaux théoriques qui se sont attachés à proposer un cadre formel pour le test. Comme problématiques de recherche majeures du domaine, on peut citer la caractérisation du processus et des politiques de test, le problème de la validité de l’extrapolation des résultats de test, la conception des données de test, leur automatisation et le problème de l’oracle. Des algorithmes et techniques ont été proposés pour concevoir et générer (automatiquement) des données de test pour certains critères.

Mots clé : test, ordonnancement temps-réel, model-checking

Structure générale et contenu

  • Contexte d’utilisation des analyses et tests formels pour le développement de logiciel. Enjeux et problématique des méthodes formelles dans les cycles de développement de logiciels industriels. (2h, Philippe Dhaussy).
  • Théorie et analyse d’ordonnancement. Cas des systèmes mono-processeurs et répartis. Tâches dépendantes et indépendantes. Relation avec les langages de conception, les langages de programmation et les systèmes d’exploitation temps réel.(6h, Frank Singhoff).
  • Modèles à processus communicant. Modèles à automates temporisés, langages réactifs asynchrones. Logiques temporelles et temporisées. Techniques de vérification par exploration de l’espace d’états (model checking). Exemple d’outil : le vérificateur UPPAAL. (6h, Philippe Dhaussy).
  • Approche formelle du test : notions de testabilité, critères de test, objectifs de test, hypothèses de test, politiques et architectures de test, mesures de couverture. Test statique. Test dynamique (structurel, fonctionnel, statistique). Approche « Model-Based Testing ». Exemple de l’automatisation de la génération des données de test comme problème de satisfaction de contraintes. (6h, Valérie-Anne Nicolas).

Références bibliographiques

  • Clarke E., Grumberg O., Peled D., Model-Ckecking, The MIT Press, Cambridge, Massachussetts, 1990.
  • B. Beizer, "Software Testing Techniques", 2nd Edition, Van Nostrand Reinhold, 1990.
  • C. L. Liu and J. W. Layland. Scheduling Algorithms for Multiprogramming in a Hard Real-Time Environnment. Journal of the Association for Computing Machinery, 20(1):46--61, January 1973.
  • Méthodes formelles : http://archive.comlab.ox.ac.uk/formal-methods.html
  • J.F. Monin, Comprendre les méthodes formelles, Masson, 1996.
  • Alur R, Dill D, A Theory of Timed Automata, Theoretical computer Science, 126(2):183-235, 25 April 1994.
  • Abrial J.R, The B-Book: Assigning Programs to Meanings, Cambridge University press, 1996, ISNB 0 521 49619 5
  • Ph. Schnochelen, B. Bérard, M. Bidoit, F. Laroussinie et A. Petit. Vérification de logiciels : Techniques et outils du model-checking. Vuibert, 1999.
  • E. Clarke, E. Emerson and A. Sistla. Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, vol 8(2): 244-263, 1986.
  • M. Bozga, S. Graf, and L. Mounier. IF-2.0: A validation environment for component-based real-time systems. In Proceedings of Conference on Computer Aided Verification, CAV’02, Copenhagen, LNCS. Springer Verlag, June 2002.
  • J-P Katoen, Principles of Model-Checking, Univ. Of Twente, Lectures notes « System Validation », 2001.
  • Marc Utting, Bruno Legeard, Practical Model-Based Testing: A Tools Approach, Elsevier (Morgan-Kaufmann), 2007.
  • S. Xanthakis, M. Maurice, A. de Amescua, O. Houri et L. Griffet, "Test & Contrôle des Logiciels : Méthodes, Techniques & Outils", EC2, 1994.
  • M.-C. Gaudel, B. Marre, F. Schlienger et G. Bernot, "Précis de génie logiciel", Masson, 1996.
  • S. Xanthakis, P. Régnier et C. Karapoulios, "Le test des logiciels", Hermès, 2000.
  • F. Cottet, J. Delacroix, C. Kaiser and Z. Mammeri. Ordonnancement temps réel. Hermès, 2000.

Modalités d'évaluation

Contrôle continu :

  • Travail personnel (seul ou en binôme): coefficient 60% : sur un sujet choisi dans une liste de sujets proposés
  • Examen papier ou examen machine (2h) : coefficient 40% (incluant des exercices sur chaque thème traité)
Buy cheap web hosting service where fatcow web hosting review will give you advices and please read bluehost review for more hosting information.