Document Scientifique de présentation du projet

T1 : Validation par test progressif par parties de systèmes logiques

Livrable L1.1 : Algorithmes de génération et d‘exécution du test des systèmes logiques, séquentiels et temporiséés non bouclés

Livrable L1.3 : Evaluation sur études de cas industriels d'un algorithme de test progressif par parties de systèmes logiques non-bouclés dans l'environnement ControlBuild

T2 : Validation par simulation de partie opérative

Livrable L2.1 : Spécification et validation, sur études de cas, d'une méthode d'utilisation des simulateurs de parties opératives : objectifs, propriétés de sûreté de fonctionnement, taux de couverture et limitations de la simulation

Livrable L2.2 : validation par simulation de partie opérative.

T3 : Apport des techniques d'identification des SED à la validation des systèmes critiques

Livrable L3.1 : Construction de modèles formels de controleurs logiques pour le test de conformité

Livrable L3.2 : Validation fonctionnelle de contrôleurs logiques : contribution au test de conformité et à l'analyse en boucle fermée

T4 : Validation formelle de propriétés quantitatives : approche par automates

Livrable L4.1 : Etude de techniques d'analyse quantitative des modèles temporisés

Livrable L4.2 : Etudes de techniques de validation à l'exécution pour des systèmes réactifs critiques.

T5 : Validation formelle de propriétés quantitatives : approche par contraintes

Livrable L5.1 : Apport de la bio-informatique à la vérification des systèmes complexes

Livrable L5.2 : Validation formelle de propriétés quantitatives : Approche par contraintes

Livrable L5.3 : Une approche CSP pour l'aide à la localisation d'erreurs