L'idée de démontrer la correction partielle ou totale d'algorithmes
ou de programmes et les premiers outils théoriques pour ce faire remontent
aux débuts de l'informatique.
La mise en pratique effective de ces idées s'est développée
beaucoup plus récemment sous le nom de méthodes formelles,
avec l'avènement, d'une part, de formalismes suffisamment riches
pour modéliser les systèmes et exprimer les propriétés attendues
et d'autre part,
de logiciels de support facilitant la modélisation
et la vérification.
Parmi les techniques les plus développées on peut indiquer
les moteurs de réécriture,
le model checking
et l'inspection d'arbres de preuve par un noyau sûr
(qui se ramène à du type checking pour les systèmes comme Coq).
Il s'agit, in fine,
de démontrer un théorème dans une théorie appropriée
qui définit le modèle du système étudié et ses propriétés possibles.
Pour des systèmes complexes ou des algorithmes subtils,
y compris ceux qui sont mis en oeuvre dans l'industrie,
il faut parfois faire appel à des arguments sophistiqués
relevant par exemple de l'algèbre, de l'analyse ou de la théorie
des automates,
d'où l'intérêt d'outils logiciels supportant la formalisation
des mathématiques correspondantes.
Les systèmes de preuve d'ordre supérieur tels que HOL,
Isabelle/HOL ou PVS ont souligné la nécessité d'une automatisation
partielle des preuves. Les systèmes HOL intègrent des outils
spécifiques de réécriture dont les performances sont bien moins bonnes
que celles des outils de réécriture dédiés ; d'autre part leur notion de
propositions équivalentes est beaucoup plus faible que celle du calcul
des constructions ce qui oblige à utiliser des déductions pour les
étapes de raisonnement équationnel plutôt que du calcul.
Le système PVS intègre des
stratégies de preuves automatiques sophistiquées mais qui sont vues
comme des boîtes noires et donc susceptibles de réponses erronées.
Par ailleurs, il peut s'avérer très utile de travailler sur une version
abstraite des modèles, notamment pour les rendre
compatibles avec certaines techniques automatiques.
Typiquement, on se ramène à une abstraction finie
et de taille raisonnablement petite lorsque l'on veut appliquer des outils
de model checking.
L'utilisation combinée d'un outil général comme Coq ou PVS
et d'outils spécialisés
permet d'utiliser chaque technique dans son domaine de prédilection,
par exemple en formalisant rigoureusement les abstractions effectuées
lorsqu'on passe d'un modèle complet et détaillé à un modèle
simplifié pour traitement automatique.
Enfin, il est important de pouvoir présenter les résultats
ou les modèles sous une forme facile à lire et à interpréter.
Les partenaires du projet proposé ici se sont engagés dans ces
directions et ont participé activement aux avancées de l'état de l'art,
avec le développement de systèmes comme
Elan (outil de réécriture parmi
les plus performants actuellement disponibles),
Coq (assistant à la preuve en logique d'ordre supérieur reconnu
parmi les plus fiables)
ou HCMC (vérification compositionnelle d'automates temporisés par model-checking).
Parmi les progrès effectués récemment,
notamment dans le cadre du projet Calife,
on peut indiquer :
la définition d'une version modulaire du calcul des construction
inductives, qui améliorera considérablement la structuration
et la réutilisation
des développements formels effectués sous Coq ;
une meilleure compréhension de l'interaction entre la logique
d'ordre supérieur et la réécriture,
en vue de disposer à terme d'un moteur logique
beaucoup plus efficace ;
la réalisation d'une interface entre Coq et Elan,
permettant d'ores et déjà de combiner sûreté et efficacité
dans les raisonnements équationnels ;
l'automatisation des preuves, avec l'intégration
de nouvelles procédures de décision
et l'amélioration du langage de tactiques de Coq ;
la définition d'un modèle d'automates temporisés (p-automates)
permettant de spécifier une très grande classe de systèmes
temps-réel, sans contrainte dictée par les algorithmes
de vérification disponibles, puis sa formalisation sous Coq
et sous Isabelle/HOL ;
au-delà de l'intérêt propre de ce formalisme, cela a validé
la possibilité de développer une couche spécialisée au-dessus
d'un outil généraliste ;
la génération de séquences de tests à partir de p-automates ;
la réalisation d'une interface graphique pour systèmes temporisés
utilisée en commun par Coq , les outils de model checking temporisé
Kronos, Uppaal et Hytech et un outil de génération de séquence de tests ;
la validation de ces techniques sur des algorithmes relatifs
à la qualité de service en ATM et des applications
de taille plus conséquente (des protocoles multicast PGM et PIM,
définis à l'IETF).
Innovation technologique et recherche développées pour le projet
Les méthodes formelles ciblent à l'origine des propriétés fonctionnelles,
que l'on peut exprimer par une formule logique
exprimant, par exemple, une relation entre les entrées
et les sorties d'un programme séquentiel,
ou un invariant le long d'une exécution.
Le développement des codes mobiles ou embarqués soulèvent
de nouvelles
questions de sécurité liées aux propriétés quantitatives sur les
ressources engagées lors de l'exécution d'une application.
En voici quelques exemples.
Un serveur ne prend en compte une requête d'une application que si
le temps de calcul est acceptable. Pour cela, le serveur
demandera à l'application cliente un « certificat de
complexité ».
Un utilisateur veut avoir la certitude que l'application qu'il
charge sur son assistant personnel ou son téléphone mobile
pourra s'exécuter avec la mémoire disponible, et sans bloquer,
par manque de ressources, les autres applications.
Un fournisseur de composant logiciel pour un système embarqué
veut démontrer que son produit répond aux spécifications en
terme de ressource mémoire et de temps de réponse, qui sont
imposées par le constructeur.
Un programme mobile dont le temps de calcul est trop long, pose
des problèmes de sécurité fonctionnelle. Outre le fait qu'il
bloque la machine hôte, n'est-il pas en train d'attaquer le
système ?
Très concrètement, dans le cadre de Calife,
l'étude de protocoles comme PIM
a fait apparaître le besoin d'exprimer
des propriétés de nature stochastiques,
énonçant par exemple qu'avec la probabilité 99 %,
les messages sont diffusés
à tous les récepteurs dans un délai inférieur à d.
Nous sommes encore insuffisamment armés pour aborder ce genre de problème
(même si des travaux existent dans le cadre de formalismes
spécialisés comme les réseaux de Petri)
d'autant plus que les propriétés d'intérêt ont le
double aspect aléatoire et temps-réel.
Ces exemples illustrent l'importance de la maîtrise des ressources
utilisées par un système,
bien que
cet aspect ait été largement sous-estimé dans le passé.
Un problème connexe
est l'étude de la complexité en espace et en temps des programmes.
On aimerait souvent savoir, par exemple, si un programme se termine en
temps pôlynomial ou requiert un espace de calcul au pire
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 à 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
ou d'une preuve faite dans le système Elan.
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.
Une autre limitation que nous voudrions dépasser porte
sur les techniques de model checking qui doivent
faire face à l'explosion combinatoire de la taille du graphe d'états.
Ce problème est particulièrement sensible
dans le cas d'une modélisation par automates temporisés,
car l'espace des états croit en outre exponentiellement
avec le nombre des horloges.
Une solution partielle a été trouvée dans le cadre du projet
Calife : un nouveau formalisme,
celui des p-automates, à la fois compact et
expressif, s'est avéré adapté aux techniques de model-checking
traditionnel et a permis de traiter l'algorithme ABR
(Available Bit Rate) avec succès.
Toutefois, le traitement de PGM à base de p-automates fait apparaitre
un nouveau phénomène d'explosion combinatoire,
lié non plus aux contraintes temporelles, mais
au nombre d'automates mis en parallèle.
Pour contourner cette difficulté, nous voulons 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.
Le projet que nous proposons a pour ambition
d'explorer ces différents thèmes de manière cohérente,
en contribuant à la construction d'un cadre pour
raisonner sur la complexité des programmes, en particulier temps-réel,
i.e. en terme de temps d'exécution, d'espace mémoire, de nombre
d'appels récursifs d'une fonction, de valeur maximum d'un
argument,...
La définition de ce cadre permettra de dégager une notion de preuve ou
de certificat des ressources consommées par un programme et par la
suite, de prendre en compte, lors de la compilation d'un programme, la
spécification quantitative imposée sur la ressource. Ainsi, par
exemple, un programme pourrait être compilé sous la contrainte de
calculer sans demande d'allocation mémoire.
Ces idées seront validées sur des applications réelles,
par exemple PIM pour la vérification de propriétés temps-réel
et probabilistes.
A titre d'application potentielle plus lointaine,
notons aussi que l'étude des performances des sytèmes
repose sur des modèles stochastiques, souvent à base
de files d'attente, modèles qui induisent toujours des hypothèses
simplificatrices (afin, par exemple, d'accélérer les simulations
en vue d'obtenir des résultats statistiquement significatifs).
Or
il n'existe pas encore de cadre formel unificateur qui pemettrait
de s'assurer de la cohérence entre un modèle
de performances et le modèle fonctionnel d'origine.
Les outils considérés pour ce projet s'appuient sur la théorie de la
complexité implicite et sont basés sur des systèmes de type, des
ordres de terminaison, ou encore des modélisations par réseaux de
Petri.
