Responsable : Burkhart Wolff
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 :
“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.
Des méthodes de génération test sont de complexité exponentielle en général. . .
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.
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.
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.
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
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.
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.
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.
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.
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.
