Pôle Modèles Test Formel et Monitoring

Responsable : Burkhart Wolff

Description

Cette thématique de recherche concerne l'utilisation des méthodes formelles pour générer des tests a partir des specifications ou programmes. Ceci inclut les aspects suivants :

  • tests dynamiques (run-time) et tests statiques (generation des tests)
  • tests unitaires, sequentielles, et adaptives
  • test techniques : exploration aléatoires, execution symboliques, raffinement, model-checking ...
  • composition de techniques et de formalismes
  • critères de couverture, méthodologie
  • utilisation conjointe de techniques de test et de preuve
  • Le test dans le genie logiciel formel et dans des processus de certification

News

New Project on Safety in Autonomous Cars

“How can we model autonomous cars in the most general way and establish the absence of catastrophic events? How to preserve such safety properties under extensions of the model?" This question marked the beginning of a fruitful partnership with SystemX on projects like SVR and now 3SA involving industrial partners such as transdev, Renault and PSA.

Read more...

Members

Permanent

PhD Students

Benoit Ballenghien

Nicolas Meric

Mots-clefs

  • Modèles et Programmes
  • Systèmes concurrentes, complexes et critiques
  • Combination des methodes de test, de preuve et de vérification algorithmique
  • Tests a base des randomisations
  • Test Refinement
  • Tests à base des Ontologies
  • Tests dans le Génie Logiciel Formel et Certifications

Détails

Composition des Méthodes Composition

Des méthodes de génération test sont de complexité exponentielle en général. . .

Méthodologie des Test Méthodologie

Dans des processus de certification des logiciels ou des systèmes embarques, la combinaison de différentes techniques de test est obligatoire, mais très peu analysé. L'objectif de cet axe de recherche (en partie avec des partenaires industrielles) est de formaliser les "test-plans" sous forme des ontologies, de développer du support sur cette base et de trouver des optimisations.

Vérification par Test et Preuve Vérification

La combinaison des méthodes de test et preuve a attiré l'intérêt de toute une communauté de chercheurs (voir la conférence [https://tap.sosy-lab.org/2020/ | Test and Proof]). Cela couvre les techniques de preuve pour la justification de test-stratégies et de critères de couverture, les techniques d’exécution symbolique et de résolution des contraintes, et la génération d'invariantes pour améliorer l'efficacité des tests randomisés pour des programmes.

Méthodes de synthèse et vérification de testsVA

Les méthodes vérification algorithmique peuvent être utilisées pour synthétiser des suites de tests (par exécution symbolique, exploration/énumération de modèle) ou pour vérifier que les tests écrits par un humain satisfont les critères de qualité imposés (par exemple, couverture, indépendance de l'ordre d'exécution). Pour cela, ces techniques de vérification doivent être adaptées pour générer des informations pertinentes pour le test. Par exemple, les procédures de décision utilisées par l'exécution symbolique doivent fournir des modèles dans une classe permettant, par énumération des traces ou des instances, de générer des entrées des systèmes sous test. L'analyse statique peut être utilisée pour inférer des propriétés invariantes du programme sous test qui sont adaptées à la synthèse de tests (accessibilité, intervalles de valeurs). De même, elle peut être utilisée pour analyser le déterminisme des tests unitaires par rapport à leur environnement d'exécution.

Exemples

Model-based Testing in HOL-TestGen

HOL-TestGen is a test case generator, built on top of Isabelle/HOL, for allowing unit and sequence testing from (functional) models written in HOL. It allows one to

  • write test functional specifications
  • (semi-) automatically partition the input space, resulting in abstract test cases,
  • automatically select concrete test data via constraint-solvers
  • automatically generate test scripts.

Test by monitoring des composantes hétérogènes polytimed et polychromes

Le langage TESL est un langage de spécification polychrone et temporisé pour décrire la causalité et les contraintes temporelles entre événements survenant dans différents composants d'un système. Une sémantique dénotationnelle et une sémantique opérationnelle ont été définies pour TESL en Isabelle/HOL, avec preuve de propriétés sur ces sémantiques. Le framework est utilise pour un système de monitoring a base des techniques symboliques, appellé Heron Solver. L'approche est censé d'être étendu par des événements avec valeurs, ce qui peut le faire applicable pour des approaches de monitoring des systèmes hybrides.

Rukia is a C++ library for model exploration by uniform random walk.

[TODO]

Auguste++ is a white-box statistical testing tool for C programs.

[TODO]

Program-based Tests in Clean

Isabelle/C/Clean is a framework for white-box test and proof of C programs. Reçemment, la plateforme Isabelle/C Project Page F-IDE Paper a été développé a l'intérieur du Isabelle framework qui permet de developper des programmes de C11 de taille conséquente. La syntaxe abstraite interne est compile dans differentes "semantic backends", i.e. theories en Isabelle offrant une semantiques pour C, qui varient dans le sous-ensemble du language, le model de memoire, et le model d'execution. Un model parmi d'eux, le model Clean, est particulièrement approprié pour l'execution symbolique qui sont utilisés dans Tactic Program-Based Testing and Bounded Verification in Isabelle/HOL; l'objectif de cette linie de recherche est de combiner ces techniques avec des techniques de generation d'invariantes de "reacheability" utilise pour le test randomisés Infeasible Paths Elimination by Symbolic Execution Techniques.

Test de propriétés des primitives shell POSIX

Dans le cadre du projet ANR Project CoLiS (fini en 2020), les primitives shell pour la manipulation du système de fichiers ont été spécifiées formellement, sur la base de la norme POSIX, dans une logique d'arbres. Toutefois, pas toutes les implémentations de ces primitives sont alignées sur la norme POSIX. D'un autre côté, la spécification donnée ne concerne que la structure du système de fichiers et ne prend pas en compte des caractéristiques comme les 'timestamps' des modifications. En se basant sur la procédure de décision de cette logique, nous étudions des méthodes pour générer des tests (système de fichiers et commande) qui indiquent la conformité d'une implémentation avec la spécification extraite de la norme POSIX.

Tests friables

Dans le cadre d'un projet de Giovanni Bernardi financé par le CNRS, nous étudions des méthodes d'analyse statique pour analyser les propriétés (déterminisme, indépendance de l'environnement) des tests unitaires écrits en C et Java. Ces méthodes sont développées dans l'analyseur Infer (logiciel libre) de Facebook.

Activities

Le Test Club est un groupe informel de discussion sur les thèmes autour du test basés sur des méthodes formelles. Dans le passé on a discuté des thèmes autour de model-based testing, program-based testing, random-based testing, model-checking, and counter-example generation.