From 6742003891028d566edf23dc7092c34f6d40255f Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Thu, 24 Jul 2014 10:18:30 +0200 Subject: Plug into Apron Box domain for intervals. --- doc/readme.pdf | Bin 236320 -> 263955 bytes doc/readme.tm | 224 ++++++++++++++++++++++++++++++++++++++++----------------- 2 files changed, 157 insertions(+), 67 deletions(-) (limited to 'doc') diff --git a/doc/readme.pdf b/doc/readme.pdf index 4a97029..aa680ca 100644 Binary files a/doc/readme.pdf and b/doc/readme.pdf differ diff --git a/doc/readme.tm b/doc/readme.tm index 8622a9a..f21a66c 100644 --- a/doc/readme.tm +++ b/doc/readme.tm @@ -823,20 +823,22 @@ peut être caractérisée par sa fonction de concrétisation : <\eqnarray*> - >>||\\|)>>>>> + >||\\|)>>>>> \ On peut aussi généralement s'appuyer sur l'existence d'une fonction d'abstraction : <\eqnarray*> - >>|||)>\\>>>> + >|||)>\\>>>> Cette fonction fait correspondre à une partie de > sa - meilleure approximation dans le domaine abstrait (par exemple dans le cas - des polyèdres, l'abstraction d'un ensemble fini de points est leur - enveloppe convexe, mais un cercle n'a pas de meilleure abstraction). + meilleure approximation dans le domaine abstrait, lorsque celle-ci existe + (par exemple dans le cas des polyèdres, l'abstraction d'un ensemble fini de + points est leur enveloppe convexe, mais un cercle n'a pas de meilleure + abstraction). En pratique la fonction d'abstraction n'est pas très + utilisée. Dans tous les cas, on s'attend à ce que x\\,x\\|)>> @@ -1441,11 +1443,65 @@ Dans ce cas, on s'arrête si =s>. - + - Une autre approche à base de partitionnement dynamique a été tentée, mais - elle n'a pas donné de très bons résultats par manque d'une heuristique sur - les partitionnements à effectuer. Détails à venir. + Une autre approche à base de partitionnement dynamique a été tentée (cf + ), mais elle + n'a pas donné de très bons résultats par manque d'une heuristique sur les + partitionnements à effectuer. + + L'idée de base consiste à se donner une liste de conditions + ,d,\,d> qui définissent + parties de > (en principe disjointes, mais les + approximations mènent parfois à des recoupenents). On étudie les parties + (ou ) =|d|\>|)>> + comme un système de transitions pour lequel on calcule un point fixe par + itérations chaotiques. + + Les conditions > sont données par une heuristique qui + découpe à chaque rafinement un des lieux > en + plusieurs sous-lieux. + + Le découpage de base est généralement : init + ; non init et propriété vérifiée ; non init et propriété non vérifiée. + + On note \S> + si dans notre sur-approximation on peut être à un cycle dans + > et dans le suivant dans >. + + On recherche un lieu > et une condition + apparaissant dans le programme (ou la négation d'une telle condition) tel + qu'il existe un état > ayant les propriétés + suivantes : + + <\eqnarray*> + >|>|>>|>|>||c|\>S>>>> + + + On peut aussi le faire dans l'autre sens : + + <\eqnarray*> + >|>|>>||c|\>S>|>|>>>> + + + Si une telle condition est détectée, alors on peut diviser le lieu + > en deux parties, + |c|\>S> et + |\c|\>S>, + c'est-à-dire qu'on pose comme nouvelles définitions + ,\,d,c\d,\c\d,d,\,d>. + On refait ensuite un point fixe. Notre analyse est en principe plus fine, + donc on espère trouver des lieux inacessibles. + + En pratique ça ne marche pas très bien car les + rafinements ne sont pas effectués dans le bon ordre. Dans le papier + sus-cité, une double analyse en avant et en arrière était utilisée pour + trouver l'intersection des valeurs accessibles depuis l'état initial et + co-accessibles jusqu'à un état qui provoque une erreur (ie dont la + définition est : la propriété est violée), mais nous n'avons pas tenté + d'implémenter une telle analyse, qui serait sans doute bien plus précise. + Remarquons que l'implémentation de pour LUSTRE est + disponnible sur sa page web (c'est l'outil NBac). @@ -1463,13 +1519,20 @@ logique ; quelques simplifications sur les formules logiques (, ). - domaine numérique non-relationnel basé sur les intervalles ; - domaine relationnel basé sur la bibliothèque externe Apron - (, , - , ...) + trois domaines numériques basés sur Apron : intervalles, polyèdres + et octogones () + + vestige d'une implémentation \S maison \T d'un domaine + non-relationnel à base d'intervalles (, + , + , ) - deux domaines abstraits et analyseur statique correspondant - (, ) + deux domaines abstraits à disjonctions et procédures d'analyse + statique correspondantes (, + ) + + procédure d'analyse par partitionnement dynamique + () En nous basant sur les options de la ligne de commande, nous allons @@ -1518,8 +1581,10 @@ en s'appuyant sur le domaine non-relationnel à base d'intervalles pour la partie numérique - : de même mais utilise le domaine abstrait - relationnel basé sur Apron (polyèdres) pour la partie numérique + : de même mais utilise le domaine abstrait + relationnel basé sur les polyèdres d'Apron pour la partie numérique + + : de même mais utilise les octogones @@ -1534,10 +1599,17 @@ : affiche encore plus de détails n\> : définit un délai pour les - opérations de widening (par défaut 5) + opérations de widening (par défaut 5). Ce délai est utilisé à deux + endroits différents de l'analyse : pour le point fixe local de chaque + itération chaotique, et pour le point fixe global des itérations. vars\> : variables à utiliser comme - variables de disjonction (par défaut : aucune) + variables de disjonction (par défaut : aucune). Donner comme argument + permet d'utiliser toutes les variables énumérées pour les + disjonctions. Donner comme argument > permet + d'utilsier toutes les variables énumérées qui sont utilisées dans une + mémoire. On peut aussi utiliser la syntaxe pour + rajouter des variables aux variables mémoire. scopes\> : donne un certain nombre de scopes pour lesquels ne pas introduire de variable @@ -1568,8 +1640,10 @@ utilisant le domaine à base d'EDD et en utilisant les intervalles comme domaine de valeurs numériques - : de même mais utilise le domaine abstrait - relationnel basé sur Apron (polyèdres) pour la partie numérique + : de même mais utilise le domaine abstrait + relationnel basé sur les polyèdres d'Apron pour la partie numérique + + : de même mais utilise les octogones @@ -1590,10 +1664,7 @@ - Une troisième forme d'analyse, basée sur un partitionnement dynamique de - > a été tentée. Celle-ci n'a pas donné de très bons - résultats, mais nous indiquons néanmoins son existence ici. - L'implémentation existe dans . + Cette analyse est implémentée dans . @@ -1606,7 +1677,7 @@ utilise des graphes de décision pour représenter les conditions sur les énumérées et les intervalles pour la partie numérique - + : utilise les polyèdres d'Apron @@ -1670,7 +1741,7 @@ ...) que l'on exécuterait comme pré-processing sur le programme. - + <\itemize> , > > > - > - > - > - > - > - > - > - > + > + > + > + > + > + > + > + > > - > - > - > - > - > - > - > - > - > - > + > + > + > + > + > + > + > + > + > + > > + > + > + |\>|?>> > > > @@ -1876,61 +1950,77 @@ |.>>>>|> > - |math-font-series||6Implémentation> - |.>>>>|> + |math-font-series||6Partitionnement + dynamique> |.>>>>|> - |6.1Parsing et affichage de + |math-font-series||7Implémentation> + |.>>>>|> + + + |7.1Parsing et affichage de programmes SCADE |.>>>>|> - > + > - |6.2Interprète SCADE + |7.2Interprète SCADE |.>>>>|> - > + > - |6.3Analyse statique par + |7.3Analyse statique par interprétation abstraite |.>>>>|> - > + > - |6.3.1Domaine à disjonctions + |7.3.1Domaine à disjonctions simples |.>>>>|> - > + > |Modes d'analyse |.>>>>|> - > + > |Options de l'analyse |.>>>>|> - > + > - |6.3.2Domaine à disjonction par + |7.3.2Domaine à disjonction par graphe de décision |.>>>>|> - > + > |Modes d'analyse |.>>>>|> - > + > |Options de l'analyse |.>>>>|> - > + > - |6.3.3Analyse par partitionnement + |7.3.3Analyse par partitionnement dynamique |.>>>>|> - > + > |Modes d'analyse |.>>>>|> - > + > |Paramètres de l'analyse |.>>>>|> - > + > + + |math-font-series||8Prolongements + envisageables> |.>>>>|> + + + |8.1Analyse des propriétés des + nombres flottants |.>>>>|> + > + + |8.2Analyse de programmes \S + taille réelle \T |.>>>>|> + > - |math-font-series||Bibliographie> + |math-font-series||9Références> |.>>>>|> - + \ No newline at end of file -- cgit v1.2.3