Rapprocher les méthodes formelles,
l’analyse statique et les tests
29 mai 2012
Le projet Hi-Lite
Tests
unitaires
Combiner tests
et preuves
Renforcer mutuellement
tests et analyse statique
Hi-Lite
Analyse
statique
Preuves
formelles
Faciliter la preuve
formelle grâce à
l’analyse statique
Un language commun d’annotation
Travail de la deuxième
année des partenaires
Résumé
d’ensemble
Rapport d’activité par tâche
•
T1 : Management et dissémination
•
•
Gestion de projet
Dissémination des produits du projet
•
•
•
•
Forge Hi-Lite : http://forge.open-do.org
Mailing listes, dépot de sources, …
Nombreuses publications et participations à des
conférences
T2 : Spécifications
•
Exigences collectées l’année dernière, affinées
cette année
Rapport d’activité par tâche
•
T3 : Langages
•
•
•
ALFA, E-ACSL manuels de référence mis à jour
Extensions SPARK
T4 : Traducteurs
•
•
•
Gros progrès sur le traducteur ALFA vers Why (gnat2why)
Support complete de ALFA dans GNAT Pro
Greffon Frama-C: E-ACSL vers C
Rapport d’activité par tâche
•
T5 : Outils d’analyse et de test
•
•
•
•
•
CodePeer : adaptations à ALFA ~ terminée, améliorations
Nombreuses améliorations dans GNATtest (génération d’un
framework de tests unitaires), y compris support des aspects
Test_Case
Evolutions du prouveur Alt-Ergo et de Why3
Evolutions de la plate-forme Frama-C
T6 : Bibliothèques et interfaces utilisateur
•
•
•
•
Intégration de gnatprove et gnattest dans GPS
Support de ALFA dans GPS
Conception en cours d’un outil de consolidation des résultats
Améliorations dans AltGr-Ergo
Rapport d’activité par tâche
•
T7 : Applications industrielles
•
•
•
•
Outils (gnatprove/gnat2why, gnattest, GPS, why3, alt-ergo,
greffon e-acsl) mis à disposition
Retour d’expérience, mises à jour disponibles
Etudes de cas : Thales, Astrium
Application des outils sur eux-mêmes
•
Utilisation de CodePeer sur CodePeer, GNAT, GPS
Praxis Work Package
•
•
Extensions du langage SPARK dans le but
d’améliorer les techniques de preuve, support
d’ALFA, et de la bibliothèque des conteneurs, par
exemple:
-
Invariants de type
-
Génériques
Développement et intégration de “Victor” un
traducteur des conditions de vérification SPARK vers
le format SMT-Lib afin de facilite l’utilisation de
démonstrateurs de théorèmes alternatifs, par
exemple Alt-Ergo.
Progrès du Praxis Work Package
Les génériques
•
•
•
•
Implémentation des génériques est en cours de
développement par Gaétan Allaert d’Altran-Praxis France.
SPARK Generics LRM et le document SPARK Generics
User View ont été publiés.
Implémentation par étapes: la dernière version de l’outil
SPARK a été délivrée en Décembre 2011 avec support des
sous-programmes génériques SPARK.
La fonction générique Ada.Unchecked_Conversion a été
étendue afin de supporter dans le contexte de preuve la
possibilité d’appliquer une pré et une post conditions à
l’instanciation.
Progrès du Praxis Work Package
Les génériques
•
Les activités de validation de la version incluent:
•
•
•
à travers le tests, l’ajout d’un ensemble considérable de
tests dans le but de valider l’implémentation des sousprogrammes génériques;
l’ajout d’annotation de preuve au nouveau code et au
code modifié par l’analyse des sous-programmes
génériques. Les conditions de vérification qui en résulte
ont été déchargées en utilisant les outils de preuve
SPARK, y compris Victor et Alt-Ergo.
L’implémentation des paquetages génériques se poursuit et
devrait être disponible dans la prochaine version de l’outil
SPARK.
Les generiques SPARK
•
•
•
•
Les génériques comme décrit dans le "SPARK Generics
LRM" sont inclus dans la nouvel édition de “SPARK: The
proven approach to High Integrity Software” par John
Barnes, que sera publié durant Q3 2012.
Les génériques SPARK excluent certaines caractéristiques
d’Ada qui ne sont pas autorisées en SPARK mais gardent
un sous-ensemble utilisable.
L’accent a été placé afin de supporter les caractéristiques
nécessaires à supporter une implémentation utilisable de la
bibliothèque des conteneurs SPARK.
Supporter le concept of démontrer une seul fois utiliser
plusieurs fois.
Progrès du Praxis Work Package
Bibliothèque SPARK
•
Tous les composants de la bibliothèque inclus dans la
dernière version de l’outil SPARK sont:
•
•
•
•
•
•
•
SPARK.Ada.Strings.Unbounded
SPARK.Ada.Command_Line
SPARK.Ada.Text_IO
Ada.Interfaces, Ada.Interaces.C
Ada.Character.Handling, SPARK.Unsigned
Une première spécification de la bibliothèque des
conteneurs a été écrite et sera mis à jour suivant le travail
réalisé par AdaCore concernant la preuve des programmes
utilisants les conteneurs.
La bibliothèque des conteneurs SPARK sera implémentée
des que les paquetages génériques seront disponible en
SPARK.
Progrès du Praxis Work Package
Support pour ALFA
Amélioration des techniques de preuve
•
Unification de la sémantique entre ALFA et SPARK pour les
pré & post conditions ainsi que pour les expressions dans
les autres contextes de preuve
ALFA a une sémantique exécutable.
SPARK est basé sur une sémantique mathématique.
Des réunions entre AdaCore et Altran Praxis ont été
tenues avec succès dans le but de définir une approche
commune.
−
−
−
•
Riposte – un générateur de contre-exemples a été
développé par Altran Praxis (non financé par le projet HiLite) et des investigations ont été menées pour le rendre
disponible avec une interface Why dans le cadre de la
technologie Hi-Lite.
Buts principaux du projet Hi-Lite (rappel)
- combiner les techniques de test logiciel et de vérification formelle
- appliquer ces techniques aux programmes mixtes Ada + C
Contributions visées par le CEA LIST dans ce contexte
- définir un langage de spécifications exécutables pour le C, EACSL, fondé sur le langage ACSL existant
- implanter un traducteur d'E-ACSL vers C
- améliorer la plateforme Frama-C dédiée à l'analyse statique de
programmes C
E-ACSL
Executable ANSI/ISO C Specification Language
- langage d'annotations exécutables pour le langage C
- annotation exécutable = traductible en une expression C évaluable
à l'exécution
- le plus possible sémantiquement compatible avec ALFA
- fondé sur le langage ACSL (ANSI/ISO C Specification Language)
- défini au cours de la 1ère année du projet
- amélioration au cours de cette seconde année
- nouvelle version du manuel de référence (version 1.5-4) à partir de
laquelle une implantation a été effectuée
- Une publication soumise
M. Delahaye, N. Kosmatov and J. Signoles. Towards a Common
Specification Language for Static and Dynamic Analyses of C
Programs. Submitted to QSIC 2012.
Traducteur d'E-ACSL vers C
- nouveau greffon de la plateforme Frama-C
- traduire les annotations E-ACSL en C pour permettre la vérification
d'assertions à l'exécution : runtime assertion checking
- utilisation d’entiers GMP (entiers mathématiques) pour être fidèle à
la sémantique d’E-ACSL.
- schéma de traduction non trivial.
- prise en compte d’une grande partie d’E-ACSL, à l’exception
notable des constructions liés à la mémoire et aux réels.
- version 0.1 distribuée en open source en janvier 2012.
- amélioration en cours et prévue pour la fin du projet :
-système de types pour générer un code beaucoup plus efficace
-support des constructions liées à la mémoire
Évolution de la plateforme Frama-C
- nouvelle version publique de Frama-C : version Nitrogen-20111001
- version requise par le traducteur d’E-ACSL en C
- nouveaux mécanismes facilitant les collaborations inter-analyses
pour la vérification de propriétés et améliorant le retour utilisateur
- une publication acceptée et deux soumises :
P. Cuoq, D. Doligez and J. Signoles. Lightweight Typed Customizable
Unmarshaling. ML Workshop 2011.
L. Correnson and J. Signoles. Combining Analyses for C Program Verification.
Submitted to FMICS 2012.
P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles and B. Yakobowski.
Frama-C: a Program Analysis Perspective. Submitted to SEFM 2012.
Résumé des travaux du CEA LIST
- nouvelle version du langage de spécifications exécutables E-ACSL
- distribution open source de la version 0.1 du traducteur d’E-ACSL en C
- évolution de la plateforme Frama-C : version Nitrogen-20111001.
- requise par le traducteur
- collaboration inter-analyses
- dissémination scientifique : 1 publication et 3 soumises sur les
thématiques Hi-Lite
- à venir :
- poursuite du travail d’implantation
- vérification programmes Ada + C
Stratégie de Thales dans le projet
•
Intégrer les approches Hi-Lite dans l’outillage Thales pour la
génération d’applications
•
•
•
Remontée des spécifications formelles dans les modèles
Adaptation du code généré pour le rendre conforme à HiLite
Évaluer cette intégration sur un cas d’étude du domaine
spatial
Nouvelle spécification du code à générer
•
Mise au point d’un prototype de code adapté aux
contraintes d’Hi-Lite
•
Masquage des pointeurs dans les structures
•
Conservation des fonctionnalités (presque) à l’identique
•
•
Discussions avec les équipes industrielles pour l’adoption
du nouveau code
En cours d’évaluation par rapport aux outils Hi-Lite
Intégration dans l’approche de modélisation
Specifications
•
Définition d’un méta-modèle
pour les spécifications
formelles
•
Préparation des
expérimentations sur la
modélisation
C2
instance 1
C1
instance 1
C2
instance 2
Tâche 1
Processus 1
Cas d’étude
•
•
Délimitation du cas d’étude
•
Contrôle de régulation thermique dans le logiciel de vol
•
Assemblage de composants et code d’implémentation
Objectifs
•
•
Évaluer l’intégration des outils Hi-Lite dans l’approche de
modélisation
Étudier les possibilités de spécifications systématiques
sur le code généré
Astrium activities in Hi-Lite
•
•
•
Industrial user
Task 2.1: “Specifications”
•
Definition of the industrial needs for the
development of critical real time embedded
software in the space domain
 Finalized in 2012
Task 7.2: “Industrial applications”
•
Validation of the Hi-Lite approach
 Definition of toy examples to validate
some specific concepts
 Definition of a “realistic” application
Task 2.1: “Specifications” (1/2)
• Analysis of standards
• ECSS-E-ST-40C (« Space engineering – Software »)
• ECSS-Q-ST-80C (« Space product assurance – Software
product assurance »)
•
•
Main conclusions
•
•
Test shall be the main validation techniques
Formal proof is accepted and sometimes recommended
Validation & verification objectives
•
Exhaustive detection of run-time errors, traceability
between test cases and test procedures, etc.
 Important number covered by Hi-Lite
Task 2.1: “Specifications” (2/2)
•
•
•
Astrium general needs
•
•
Decrease of costs and delays
Increase of the quality
More specific needs
•
•
•
•
•
Validation of generic software / customised software
Safe reuse of software building blocks
Verification of the sensor data
Properties on vectors
Etc.
Used Ada features
•
•
Mathematical operators, arrays, ...
Generics, discriminant records, expression functions, ...
ECS
Task 7.2: “Industrial applications” (1/3)
MVM
TM/TC
GNC
EAP
EPC
EAP
EAP
EPC
EAP
ECS
TC
TM
Environment
ECS
EPC
Sensors
Navigation
Guidance
Control
Actuators
Mission & Vehicle Management
MVM
Telemetry / Telecommand
TMTC
Task 7.2: “Industrial applications” (3/3)
Algorithms
•
•
Orientation of the ATV solar wings
•
Optimisation of energy
Experimentations in SPARK
•
Comparison with Hi-Lite
Generic
Discriminant
Contract
Test cases
Formal proof
Tests
Travail à venir
Travail pour cette année
•
•
•
Tâches 4 (traducteurs), 5 (outils analyse/test) et 7
(bibliotheques, IHM) en pleine charge
Finalisation des tâches 2 (spécifications) et 3 (langages)
Début de la tâche 7 (applications industrielles)
Questions ?
Descargar

Slide 1