Précédent Remonter Suivant
Description technique du projet

Lot 1 : architecture, intégration

Partenaires impliqués

Ce lot rassemble l'ensemble des partenaires du projet, qui seront amenés à collaborer avec CRIL Technology, pour l'intégration de leurs systèmes au prototype et la mise en application de leurs résultats.

Responsable
CRIL Technology (Bertrand Tavernier)

Objectifs

Le lot 1 vise à définir et développer une architecture logicielle permettant l'intégration des différents outils développés par les partenaires du projet et offrant à l'utilisateur une interface conviviale, l'objectif final étant de mettre les systèmes de preuve à la portée des ingénieurs concepteurs d'applications critiques.

Le projet Calife a permis de valider l'utilisation du standard XML pour représenter les p-automates. Ce format sera étendu à l'ensemble des objets manipulés par les différents outils du logiciel : Ce lot définira la structure XML de ces objets, sur laquelle sera ensuite construite l'Interface Homme-Machine (utilisation du format DOM du W3C). Il définira les formats d'entrée, au format texte ou XML, des systèmes de preuve (Coq et HCMC), de simulation (Elan) et de génération de test (Isabelle/Cclair et le générateur de tests developpé par le LaBRI). Cette partie comprendra également l'écriture des transformations XSL qui permettront de projeter les fichiers XML vers les formats d'entrée des outils.

Par ailleurs, ce lot mettra en place une interface d'utilisation conviviale. Cette interface offrira les fonctions suivantes :
Déroulement et fournitures
Lot 2 : applications

Partenaires impliqués

CRIL Technology, LSV, FTR&D, LORIA, PCRI, LaBRI

Responsable
FTR&D (Jean-François Monin)

L'architecture logicielle et les différentes technologies développées seront validées sur différents cas d'études fournis par les partenaires du projet. Les premiers que nous considérerons sont les protocoles multicast comme PIM ou PGM, qui ont soulevé quelques uns des problèmes évoqués ci-dessus (par exemple, la nécessité de travailler sur des propriétés temps-réel et probabilistes). Mais nous avons en vue d'autres applications, par exemple dans le domaine des systèmes d'exploitation embarqués sur des mobiles. Par ailleurs, CRIL Technology travaille avec le milieu industriel de l'aéronautique et cherchera prendre en compte des applications issues de ce domaine.

Déroulement et fournitures
Lot 3 : test, animation

Partenaires impliqués
LaBRI, CRIL, FTR&D, LORIA

Responsable
LaBRI (Patrick Félix)

Ce lot comporte différentes techniques d'exécution de spécifications : les enseignements apportés par l'animation ou la simulation sont souvent très précieux lors de la mise au point d'une spécification. La génération de séquences de tests, culturellement proche, est également considérée.

Sous-lot 1 : animation

La plate-forme développée intègrera la possibilité de visualiser graphiquement des traces d'exécution, représentées au format XML. En particulier, la partie animation utilisera la forme graphique des différents automates saisis sous l'éditeur afin de visualiser les localités, d'une part et la valuation des variables, d'autre part.

Les traces d'exécutions seront générées de différentes manière : L'utilisateur pourra ainsi visualiser le fonctionnement général du système saisi et les contre-exemples générés par le model-checker, ce qui lui facilitera grandement la mise au point des spécifications.

Le système Elan offre un cadre homogène basé sur le calcul de réécriture pour le prototypage de systèmes décrits à bases de règles et de stratégies. Il possède un interpréteur et un compilateur efficace qui permettent la traduction rapide de tout système spécifié à l'aide de règles de réécriture et de stratégies en un programme exécutable. Nous avons récemment étudié son utilisation pour le prototypage d'algorithmes de vérification de propriétés d'automates temporisés. Une extension vers la vérification de propriétés des p-automates du projet RNRT Calife a aussi été réalisée.

Il en ressort que les systèmes à base de règles comme le système Elan peuvent permettre un prototypage rapide des algorithmes de vérification. L'utilisation de ces techniques pourra donc être expérimentée comme support pour l'animation.

Déroulement et fournitures
Sous-lot 2 : test
Un effort de normalisation pour le test de protocoles et de systèmes a permis de définir une taxinomie des tests en : test de conformité (implantation conforme à la spécification), test de robustesse (capacité de l'implantation à réagir dans un environnement plus « hostile » que prévu, cas particulièrement intéressant avec les systèmes temporisés), test d'interopérabilité (capacité de plusieurs systèmes communicants à interopérer), test de performances (capacité du système à réagir correctement en optimisant les temps de communication et de réaction).

Dans le cadre du projet Calife, nous nous sommes essentiellement intéressés au test de conformité avec une approche « objectif de test » : système et objectif de test s'expriment en termes de p-automates, et une technique de produit synchronisé entre la spécification et l'objectif de test permet d'obtenir des séquences de test issues de la spécification et respectant l'objectif de test. Cette approche a permis d'aborder le test de conformité et de générer des séquences de test dans le cadre l'étude de cas ABR. Par contre, dans le cas de l'étude de cas PGM, où la modélisation fait intervenir plusieurs composants (émetteur, récepteur, noeud), il est apparu utile d'effectuer des tests d'interopérabilité : après avoir testé la conformité de différents composants indépendamment, il s'agit de connaître leur aptitude à communiquer entre eux en satisfaisant les contraintes temporelles. Pour aborder le test d'interopérabilité, nous serons amenés à identifier clairement les propriétés d'interopérabilité temporelles et à proposer un schéma de répartition de test, avec éventuellement une coordination entre plusieurs observateurs.

L'objectif de ce sous-lot est de mettre en oeuvre une technique de génération de test d'interopérabilité pour les p-automates en s'inspirant des approches connues dans le cadre des automates classiques. La solution mise en ouvre utilisera naturellement les méthodes de modélisation compositionnelle du sous-lot « modélisation compositionnelle » du lot 4 (technologie de modélisation) et pourra exploiter les techniques de vérification compositionnelle du sous-lot 2 « vérification compositionnelle » du lot 5 (technologie de vérification) afin d'identifier des propriétés d'interopérabilité temporelles.

Déroulement et fournitures
Lot 4 : technologie de modélisation

Partenaires impliqués

LSV, PCRI, LORIA, FTR&D
Responsable
LSV (Laurent Fribourg)

Les techniques considérées dans ce lot relèvent de la modélisation mais aussi de la vérification : il s'agira de briser la complexité de la vérification en s'appuyant la décomposition d'un modèle, ou de l'expression suivie de la vérification de propriétés non fonctionnelles.

Sous-lot 1 : modélisation compositionnelle
Le model checking, consiste à modéliser un système par un automate (ou plusieurs automates mis en parallèle), et à vérifier des propriétés du système modélisé en explorant le graphe des états de cet automate. Le problème majeur auquel doit faire face le model-checking est celui de l'explosion combinatoire de la taille du graphe d'états. Ce problème est d'autant plus sensible dans le cas d'une modélisation par automates temporisés -- des automates finis étendus avec plusieurs horloges mesurant l'écoulement du temps -- car l'espace des états croit en outre exponentiellement avec le nombre des horloges de l'automate.

Une solution partielle a été trouvée dans le cadre du projet Calife: il s'agit d'utiliser un nouveau formalisme, celui des p-automates, qui étend le formalisme des automates temporisés en intégrant certains paramètres intervenant, soit dans les contraintes de temps auquelles sont assujetties les horloges, soit dans certaines données échangées par les automates. Ce formalisme, à la fois compact et expressif, s'est avéré adapté aux techniques de model-checking traditionnel. C'est ainsi qu'une vérification complète du programme temps-réel de contrôle de trafic ABR, ainsi qu'une vérification partielle du protocole multipoint PGM (Pragmatic General Multicast) ont pu être effectuées en partant d'une modélisation sous forme de p-automates, à l'aide des outils classiques du model-checking temporisé HyTech et Uppaal.

Toutefois, le traitement de PGM à base de p-automates fait apparaitre un nouveau phénomène d'explosion combinatoire. Ce phénomène n'est plus lié au nombre des horloges ou aux contraintes temporelles, mais au nombre d'automates représentant les émetteurs, les récepteurs et les noeuds intermédiaires mis en parallèle : dès la modélisation de plus d'un émetteur et de deux récepteurs, la simulation du système global induit de nouveau un phénomène d'explosion combinatoire, qui empêche toute analyse du comportement global.

Pour contourner cette difficulté, il est naturel d'explorer la voie du model-checking compositionnel qui a déjà donné d'intéressants résultats dans le cas des automates finis traditionnels ou temporisés. L'idée est d'éviter de construire ou d'examiner l'espace des états du réseau global N=(A1 | ··· | An) résultant de la mise en parallèle de n automates. À la place, quand on a une propriété j à examiner, les composants A1,···,An sont graduellement retirés de N et incorporés dans la formule j; ainsi l'automate An est « intégré » dans j, ce qui donne une nouvelle formule quotient j/An représentant ce que doit satisfaire le reste du réseau (A1 | ··· | An-1). En itérant ce processus, on est amené à construire une formule quotient globale (··· ((j/An)/An-1)···/A1), qui doit être satisfaite par le réseau « vide » (n'exécutant aucune action).

L'objectif de ce sous-lot est de mettre en oeuvre des méthodes de modélisation compositionnelle pour les p-automates, en étendant les méthodes connues pour les automates temporisés classiques. Cela impose de concevoir une logique de spécification des comportements étendue aux p-automates. Cela suppose également la mise au point de stratégies de simplification pour réduire la taille des formules quotients intermédiaires dans ce cadre. Cela requiert enfin de développer des méthodes de résolution pour vérifier la formule quotient ultime.

Déroulement et fournitures
Sous-lot 2 : probabilités

La spécification et modélisation de systèmes temps réel nécessite souvent de faire intervenir des facteurs probabilistes dans la modélisation de l'environnement, des comportements ou des pannes. Les calculs de probabilités demandent des outils mathématiques avancés. Les environnements de preuve actuels n'ont pas été conçus pour prendre en compte des propriétés probabilistes. L'un des objectifs de ce projet est de mettre en place des bibliothèques Coq permettant de raisonner sur les objets de base des probabilités, ces bibliothèques s'appuient sur les développement actuels de la théorie des réels pour Coq. Dans un second temps ces bibliothèques seront utilisées dans la modélisation d'un système temps-réel. Un candidat évident à cette modélisation est le protocole PIM.

Une approche complémentaire est issue des techniques de réécriture. Depuis une décennie, les langages à base de règles comme Elan se sont focalisés sur l'utilisation de la réécriture comme un outil de modélisation qui permet l'exécution de spécifications. Ces outils ont été étudiés essentiellement pour la modélisation de systèmes réactifs discrets. Il est important de savoir modéliser les systèmes qui font intervenir des choix probabilistes avec ces langages. L'un des objectifs du projet concerne l'extension du système Elan pour la modélisation des systèmes à base de probabilités.

Utiliser des systèmes à base de règles probabilistes pose de nouveaux problèmes théoriques qui restent à comprendre. Nous avons ainsi étudié la généralisation des résultats de réécriture classiques pour une notion de systèmes abstraits de dérivations probabilistes.  Une compréhension fine de ce que pourrait donner la généralisation des différentes notions de la réécriture (relation de réécriture, logique de réécriture, calcul de réécriture) lorsque le déclenchement des règles est sujet à des choix probabilistes est proposée.

Par ailleurs, l'utilisation de règles probabilistes permet le prototypage et l'utilisation de techniques probabilistes pour la vérification ou l'analyse de systèmes, qu'ils soient probabilistes ou non-probabilistes. Nous proposons d'étudier dans ce cadre l'utilisation de techniques probabilistes pour l'analyse de systèmes ou la recherche de preuve.

Déroulement et fournitures
Sous-lot 3 : complexité en espace et en temps
La preuve de programme a pour but de répondre par oui ou par non à la question de savoir si un programme donné se termine et satisfait une spécification donnée. Mais on aimerait souvent avoir des réponses plus quantitatives, comme par exemple, si le programme se termine en temps polynomial ou pourra se contenter pour ses calculs d'un espace logarithmique. Ce problème a certes été étudié par les algorithmiciens qui ont bâti des logiciels d'évaluation d'algorithmes à partir de briques de base connues. Notre objectif est autre : nous visons a extraire des information sémantiques, visant plus particulièrement la consommation de ressources en temps et espace, à partir d'une preuve de correction de programme faite en Coq. L'idée est que des annotations adéquates des règles de preuve devraient permettre de réaliser cet objectif, que l'on peut voir comme une évaluation partielle de la preuve.

De façon complémentaire, nous proposons d'étudier des techniques pour permettre l'analyse de la complexité d'un programme spécifié par un langage fonctionnel du premier ordre. Par exemple, pour évaluer les resources en temps ou en espace requises pour l'exécution d'un programme spécifié dans le langage Elan, ou dans tout autre langage fonctionnel du premier ordre.

Dans ce cadre, ces techniques seront utilisées pour garantir l'utilisation des ressources des systèmes à codes mobiles et embarqués.

Participants : PCRI, LORIA

Déroulement et fournitures
Lot 5 : technologie de vérification

Partenaires impliqués
PCRI, LORIA, LSV-ENS Cachan.

Responsable
LRI (Christine Paulin)

Le travail proposé dans ce lot permettra la construction d'un système original qui combinera efficacité et sûreté des preuves. À la différence du lot précédent, l'activité de modélisation n'entre pas en compte.

Sous-lot 1 : ajouter la réécriture au noyau de calcul de Coq

Les systèmes interactifs de preuve d'ordre supérieur doivent intégrer des raisonnements équationnels de manière efficace et sûre. Or l'égalité n'est pas une notion primitive en logique d'ordre supérieur. Le raisonnement équationnel doit être traduit en des étapes élémentaires de remplacement ce qui le rend souvent très inefficace. La première nécessité est d'utiliser les techniques de pointe de compilation de réécriture telles que celles développées pour le système Elan. Le second besoin est de comprendre quel terme de preuve doit être conservé dans l'assistant de preuve pour justifier le raisonnement équationnel.

Une particularité du système Coq est la possibilité de considérer toute preuve d'une propriété P comme la preuve d'une propriété Q pour peu que Q soient équivalentes modulo un certain calcul. Ainsi une preuve de 24=24 est également une preuve de 4!=24 puisque 4=4× 3× 2 × 1=24. Une idée naturelle est de rendre équivalentes plus de formules, en intégrant, par exemple, l'associativité ou la commutativité de certains opérateurs, c'est la base de la déduction modulo. Cependant, cela ne peut se faire que si on garantit la cohérence du système logique obtenu ainsi que la décidabilité de la vérification des preuves.

Des progrès importants ont été réalisés ces trois dernières années dans la compréhension de l'interaction entre la logique d'ordre supérieur et la réécriture, en particulier dans le cadre du projet RNRT Calife. Des restrictions ont été proposées qui permettent de garantir la propriété de normalisation du système résultant. Cependant, la mise au point d'un assistant de preuve complet reposant sur ces nouvelles technologies pose encore des problèmes théoriques non triviaux comme la vérification de la cohérence de définitions, aussi elle n'est pas envisagée à court terme.

Dans ce projet, nous proposons la mise en place d'une extension du système Coq qui améliore sensiblement les performances des preuves par réécriture sans remettre en cause les fondements logiques du calcul. L'idée est de prouver des égalités sur des fonctions définies dans le calcul des constructions (on se limitera dans un premier temps à des fonctions du premier ordre), d'orienter ces équations en règles et d'intégrer un moteur puissant de réécriture à la machine actuelle de vérification de convertibilité des propositions. L'obligation de prouver les égalités (en général de manière inductive) permet de garantir la cohérence du système obtenu. Du point de vue de la terminaison, nous analyserons les différentes techniques garantissant que celle-ci est préservée (schéma général, ordre RPO d'ordre supérieur ou une adaptation du critère de paires de dépendances implanté dans CiME) pour choisir la mieux adaptée au traitement des exemples du projet.

Déroulement et fournitures
Sous-lot 2 : vérification compositionnelle

Ce sous-lot s'inscrit naturellement dans la continuation du sous-lot « modélisation compositionnelle » du lot 4 technologie de modélisation. Le lot 4, élabore des techniques de model-checking compositionnel pour les p-automates qui seront mises en oeuvre dans le cadre de ce lot.

Plus précisément, il s'agit d'étendre le système HCMC réalisé par François Laroussinie au LSV pour la vérification compositionnelle d'automates temporisés (pente des horloges égale à 1) et hybrides simples (pente des horloges égale à 1 ou à 0), au cas des p-automates. Ce sous-lot exploitera les extensions de la logique de spécification des propriétés ainsi que les techniques de simplification et résolution de contraintes, mises au point dans le lot 4.1. Nous réfléchirons également à différentes solutions pour faire interagir les méthodes de vérification propres à HCMC (et son extension) avec Coq.

Déroulement
Sous-lot 3 : mécanisation de la déduction

Les étapes de preuves des systèmes nécessitent des techniques spécialisées de model-checking mais également des preuves de logique traditionnelle (calcul des prédicats, récurrence). Le système Coq propose peu de moyens d'automatiser de tels raisonnements. La difficulté d'adapter les méthodes connues vient du fait que les connecteurs logiques ne sont pas primitifs mais sont des cas particuliers de définitions inductives générales et, de plus, il est nécessaire de produire un terme de preuve acceptable par le noyau sûr de l'assistant.

Nous aborderons ce problème selon deux méthodes. La première méthode consiste à construire une tactique de preuves couvrant uniformément les définitions inductives correspondant à des formules du premier ordre. La difficulté est de trouver une méthode qui se généralise aisément au Calcul des Constructions Inductives et permette la construction efficace de termes de preuves.

La seconde méthode utilise les résultats récents obtenus dans le cadre de la déduction modulo qui permet de combiner les techniques de preuve déductive et calculatoire.

Dans le cadre du projet Calife, nous avons spécialisé l'approche de [DHK98] pour prendre en compte la notion de redondance entre propositions basée sur les systèmes ordonnés.

Plus récemment nous avons montré comment le concept de déduction modulo permet de prendre en compte les raisonnements par récurrence. Cette approche permet de relier explicitement les techniques de récurrence implicite basées sur la réécriture telles qu'elles sont implantées dans Spike ou celles basées sur les preuves par consistance à celles utilisant explicitement des principes de récurrence.

Notre objectif sera ici de comprendre comment utiliser les résultats précédents pour étendre la puissance des principes de récurrence utilisés dans les assistants de preuve en les faisant bénéficier des techniques issues des méthodes de preuve par récurrence via la réécriture dans un premier temps ou via réécriture et consistance dans un second temps.

Déroulement et fournitures
Précédent Remonter Suivant