diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/readme.pdf | bin | 263736 -> 276546 bytes | |||
| -rw-r--r-- | doc/readme.tm | 111 | ||||
| -rw-r--r-- | doc/research.bib | 70 |
3 files changed, 151 insertions, 30 deletions
diff --git a/doc/readme.pdf b/doc/readme.pdf Binary files differindex 89e5d4e..4c2482c 100644 --- a/doc/readme.pdf +++ b/doc/readme.pdf diff --git a/doc/readme.tm b/doc/readme.tm index c6cde6d..c3fbafb 100644 --- a/doc/readme.tm +++ b/doc/readme.tm @@ -9,7 +9,7 @@ Le projet consiste en la réalisation d'un analyseur statique pour des programmes SCADE, utilisant l'interprétation abstraite comme base de - travail. Les objectifs attendus sont : + travail. Les objectifs visés sont : <\itemize> <item>Preuve de propriétés de sûreté sur des programmes @@ -17,6 +17,10 @@ <item>Étude d'intervalles de variation pour des variables </itemize> + Nos travaux se placent dans la continuité de <cite|blanchetEtAl-PLDI03>, + <cite|cousotCousot79-1>, <cite|halbwachs94c>, <cite|lesartse>, + <cite|jhrsas99>. + L'expérience a été menée sur un sous-ensemble très restreint du langage SCADE, comportant notamment : @@ -32,6 +36,8 @@ prises en compte) </itemize> + \; + Dans ce document nous mettrons au clair les points suivants : <\enumerate> @@ -59,6 +65,8 @@ Par la suite, nous ne considérons que des programmes SCADE bien typés. + \; + <section|Spécification> <subsection|Grammaire> @@ -1111,8 +1119,8 @@ Étant donné notre système représenté par une fonction de transition <math|f<rsup|#>> et une fonction de cycle <math|c<rsup|#>> (par facilité, on notera <math|g<rsup|#>=c<rsup|#>\<circ\>f<rsup|#>>), l'ensemble des - états accessible par le système est <math|S<rsup|#>=lfp<rsub|I<rsup|#>><around*|(|\<lambda\>s.I<rsup|#>\<sqcup\>g<rsup|#><around*|(|s|)>|)>>, - où <math|I<rsup|#>=<around*|\<llbracket\>|i|\<rrbracket\>><around*|(|\<top\>|)>>. + états accessible par le système est <math|S<rsup|#>=lfp<rsub|S<rsub|0><rsup|#>><around*|(|\<lambda\>s.S<rsub|0><rsup|#>\<sqcup\>g<rsup|#><around*|(|s|)>|)>>, + où <math|S<rsub|0><rsup|#>=<around*|\<llbracket\>|i|\<rrbracket\>><around*|(|\<top\>|)>>. Pour <math|d<rsub|0>\<in\>\<bbb-M\><rsub|d>>, notons <math|r<rsub|d<rsub|0>> : \<cal-D\><rsup|#>\<rightarrow\>\<cal-D\><rsup|#>> @@ -1125,7 +1133,7 @@ <item>Poser : <\eqnarray*> - <tformat|<table|<row|<cell|s<rsub|0>>|<cell|=>|<cell|I<rsup|#>>>|<row|<cell|\<delta\><rsub|0>>|<cell|=>|<cell|<around*|{|d\<in\>\<bbb-M\><rsub|d>\| + <tformat|<table|<row|<cell|s<rsub|0>>|<cell|=>|<cell|S<rsub|0><rsup|#>>>|<row|<cell|\<delta\><rsub|0>>|<cell|=>|<cell|<around*|{|d\<in\>\<bbb-M\><rsub|d>\| s<rsub|0><around*|(|d|)>\<neq\>\<bot\><rsub|0>|}>>>>> </eqnarray*> @@ -1150,7 +1158,7 @@ et non par union simple dans le futur. La définition devient alors : <\eqnarray*> - <tformat|<table|<row|<cell|s<rsub|0>>|<cell|=>|<cell|I<rsup|#>>>|<row|<cell|\<delta\><rsub|0>>|<cell|=>|<cell|<around*|{|d\<in\>\<bbb-M\><rsub|d>\| + <tformat|<table|<row|<cell|s<rsub|0>>|<cell|=>|<cell|S<rsub|0><rsup|#>>>|<row|<cell|\<delta\><rsub|0>>|<cell|=>|<cell|<around*|{|d\<in\>\<bbb-M\><rsub|d>\| s<rsub|0><around*|(|d|)>\<neq\>\<bot\><rsub|0>|}>>>|<row|<cell|K<rsub|\<nabla\>,0>>|<cell|=>|<cell|\<varnothing\>>>>> </eqnarray*> @@ -1175,7 +1183,7 @@ d'itération suivant : <\eqnarray*> - <tformat|<table|<row|<cell|s<rsub|0>>|<cell|=>|<cell|I<rsup|#>>>|<row|<cell|\<delta\><rsub|0>>|<cell|=>|<cell|<around*|{|d\<in\>\<bbb-M\><rsub|d>\| + <tformat|<table|<row|<cell|s<rsub|0>>|<cell|=>|<cell|S<rsub|0><rsup|#>>>|<row|<cell|\<delta\><rsub|0>>|<cell|=>|<cell|<around*|{|d\<in\>\<bbb-M\><rsub|d>\| s<rsub|0><around*|(|d|)>\<neq\>\<bot\><rsub|0>|}>>>|<row|<cell|K<rsub|\<nabla\>,0>>|<cell|=>|<cell|\<varnothing\>>>>> </eqnarray*> @@ -1407,7 +1415,7 @@ <\eqnarray*> <tformat|<table|<row|<cell|s<rsub|0>>|<cell|=>|<cell|\<oast\><rsub|\<bot\>> - I<rsup|#>>>>> + S<rsub|0><rsup|#>>>>> </eqnarray*> (appliquer <math|\<oast\>> de la sorte permet de faire que toutes les @@ -1445,9 +1453,9 @@ <subsection|Partitionnement dynamique> - Une autre approche à base de partitionnement dynamique a été tentée (cf - <em|Dynamic Partitionning in Analyses of Numerical Properties>), mais elle - n'a pas donné de très bons résultats par manque d'une heuristique sur les + Une autre approche à base de partitionnement dynamique a été tentée (cette + approche est décrite dans <cite|jhrsas99>)<math|>, 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 @@ -1509,10 +1517,10 @@ suivants : <\itemize> - <item>parser, lexer, typeur pour notre sous-ensemble de SCADE (source des - fichiers dans <verbatim|frontend/>) + <item>lexer, parser, typeur symple pour notre sous-ensemble de SCADE + (source des fichiers dans <verbatim|frontend/>) - <item>interprète pour la sémantique cocnrète + <item>interprète pour la sémantique concrète (<verbatim|interpret/interpret.ml>) <item>implémentation de la transformation d'un programme en formule @@ -1737,22 +1745,46 @@ ...) que l'on exécuterait comme pré-processing sur le programme. </itemize> - <section*|Références> - - <\itemize> - <item><name|N.Halbwachs>, <em|About synchronous programming and abstract - interpretation>, International Symposium on Static Analysis, SAS'94. - - <item><name|N.Halbwachs>, <name|F.Lagnier> and <name|C.Ratel>, - <em|Programming and verifying real-time systems by means of the - synchronous data-flow programming language Lustre>, IEEE Transactions on - Software Engineering, Spcial Issue on the Specification and Analysis of - Real-Time Systems, Sept. 1992 - - <item><name|B.Jeannet>, <name|N.Halbwachs> and <name|P.Raymond>, - <em|Dynamic Partitioning in Analyses of Numerical Properties>, Static - Analysis Symposium, SAS'99. - </itemize> + <\bibliography|bib|tm-plain|research.bib> + <\bib-list|5> + <bibitem*|1><label|bib-blanchetEtAl-PLDI03>B.<nbsp>Blanchet, + P.<nbsp>Cousot, R.<nbsp>Cousot, J.<nbsp>Feret, L.<nbsp>Mauborgne, + A.<nbsp>Miné, D.<nbsp>Monniaux<localize| and >X.<nbsp>Rival.<newblock> + A static analyzer for large safety-critical software.<newblock> + <localize|In ><with|font-shape|italic|Proceedings of the ACM SIGPLAN + 2003 Conference on Programming Language Design and Implementation + (PLDI'03)>, <localize|pages >196--207. San Diego, California, USA, June + 7--14 2003. ACM Press.<newblock> + + <bibitem*|2><label|bib-cousotCousot79-1>P.<nbsp>Cousot<localize| and + >R.<nbsp>Cousot.<newblock> Systematic design of program analysis + frameworks.<newblock> <localize|In ><with|font-shape|italic|Conference + Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles + of Programming Languages>, <localize|pages >269--282. San Antonio, + Texas, 1979. ACM Press, New York, NY.<newblock> + + <bibitem*|3><label|bib-halbwachs94c>N.<nbsp>Halbwachs.<newblock> About + synchronous programming and abstract interpretation.<newblock> + <localize|In >B.<nbsp>LeCharlier<localize|, editor>, + <with|font-shape|italic|International Symposium on Static Analysis, + SAS'94>. Namur (belgium), September 1994. LNCS 864, Springer + Verlag.<newblock> + + <bibitem*|4><label|bib-lesartse>N.<nbsp>Halbwachs, + F.<nbsp>Lagnier<localize| and >C.<nbsp>Ratel.<newblock> Programming and + verifying real-time systems by means of the synchronous data-flow + programming language lustre.<newblock> <with|font-shape|italic|IEEE + Transactions on Software Engineering, Special Issue on the + Specification and Analysis of Real-Time Systems>, , September + \ 1992.<newblock> + + <bibitem*|5><label|bib-jhrsas99>B.<nbsp>Jeannet, + N.<nbsp>Halbwachs<localize| and >P.<nbsp>Raymond.<newblock> Dynamic + partitioning in analyses of numerical properties.<newblock> + <localize|In ><with|font-shape|italic|Static Analysis Symposium, + SAS'99>. Venezia (Italy), sep 1999.<newblock> + </bib-list> + </bibliography> \; </body> @@ -1813,15 +1845,34 @@ <associate|auto-50|<tuple|7.1|19>> <associate|auto-51|<tuple|7.2|20>> <associate|auto-52|<tuple|<with|mode|<quote|math>|\<bullet\>>|20>> + <associate|auto-53|<tuple|3|20>> <associate|auto-6|<tuple|2.3.1|3>> <associate|auto-7|<tuple|2.3.2|3>> <associate|auto-8|<tuple|2.3.3|3>> <associate|auto-9|<tuple|2.3.4|4>> + <associate|bib-blanchetEtAl-PLDI03|<tuple|1|?>> + <associate|bib-cousotCousot79-1|<tuple|2|?>> + <associate|bib-halbwachs94c|<tuple|3|?>> + <associate|bib-jhrsas99|<tuple|5|?>> + <associate|bib-lesartse|<tuple|4|?>> </collection> </references> <\auxiliary> <\collection> + <\associate|bib> + blanchetEtAl-PLDI03 + + cousotCousot79-1 + + halbwachs94c + + lesartse + + jhrsas99 + + jhrsas99 + </associate> <\associate|toc> <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|1<space|2spc>Introduction> <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>> @@ -2025,7 +2076,7 @@ taille réelle \T <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>> <no-break><pageref|auto-51>> - <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|Références> + <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|Bibliographie> <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>> <no-break><pageref|auto-52><vspace|0.5fn> </associate> diff --git a/doc/research.bib b/doc/research.bib new file mode 100644 index 0000000..dcf93bc --- /dev/null +++ b/doc/research.bib @@ -0,0 +1,70 @@ + +@INPROCEEDINGS{halbwachs94c, + AUTHOR={N. Halbwachs}, + TITLE={About synchronous programming and abstract interpretation}, + BOOKTITLE={International Symposium on Static Analysis, SAS'94}, + EDITOR = {B. {LeCharlier}}, + PUBLISHER = {LNCS 864, Springer Verlag}, + ADDRESS = {Namur (belgium)}, + MONTH = {September}, + YEAR= 1994 +} +@ARTICLE{lesartse, + AUTHOR = {N. Halbwachs and F. Lagnier and C. Ratel }, + TITLE = {Programming and verifying real-time systems by means of + the synchronous data-flow programming language Lustre}, + JOURNAL = {IEEE Transactions on Software Engineering, + Special Issue on the Specification and Analysis + of Real-Time Systems}, + MONTH={September }, + YEAR=1992 +} +@INPROCEEDINGS{jhrsas99, +AUTHOR = {B. Jeannet and N. Halbwachs and P. Raymond}, +TITLE={Dynamic Partitioning in Analyses of Numerical +Properties}, +BOOKTITLE={Static Analysis Symposium, SAS'99}, +address={Venezia (Italy)}, +month = sep, +year=1999 +} + +\bibitem{cousotCousot79-1} +P. Cousot and R. Cousot. +\newblock Systematic design of program analysis frameworks. +\newblock In \emph{Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT + Symposium on Principles of Programming Languages}, pages 269--282, San + Antonio, Texas, 1979. ACM Press, New York, NY, U.S.A. + +@inproceedings{cousotCousot79-1, + author = {Cousot, P. and Cousot, R.}, + title = {Systematic design of program analysis frameworks}, + pages = {269--282}, + booktitle = {Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT + Symposium on Principles of Programming Languages}, + address = {San Antonio, Texas}, + publisher = {ACM Press, New York, NY}, + year = 1979, +} + + +\bibitem{blanchetEtAl-PLDI03} +B{.} Blanchet, P{.} Cousot, R{.} Cousot, J{.} Feret, L{.} Mauborgne, A{.} + Min\'e, D{.} Monniaux, and X{.} Rival. +\newblock A Static Analyzer for Large Safety-Critical Software. +\newblock \emph{Proc{.} ACM SIGPLAN 2003 Conference on Programming Language + Design and Implementation} (PLDI'03), San Diego, California , USA, June + 7--14, 2003, pp{.} 196--207. ACM Press, 2003. + +@InProceedings{blanchetEtAl-PLDI03, + author = {B. Blanchet and P. Cousot and R. Cousot and J. Feret and + L. Mauborgne and A. Min\'e and D. Monniaux and X. Rival}, + title = {A Static Analyzer for Large Safety-Critical Software}, + pages = {196--207}, + booktitle = {Proceedings of the ACM SIGPLAN 2003 Conference on Programming + Language Design and Implementation (PLDI'03)}, + address = {San Diego, California, USA}, + publisher = {ACM Press}, + month = {June 7--14}, + year = 2003, +} |