summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/readme.pdfbin263736 -> 276546 bytes
-rw-r--r--doc/readme.tm111
-rw-r--r--doc/research.bib70
3 files changed, 151 insertions, 30 deletions
diff --git a/doc/readme.pdf b/doc/readme.pdf
index 89e5d4e..4c2482c 100644
--- a/doc/readme.pdf
+++ b/doc/readme.pdf
Binary files differ
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,
+}