From 818c737eb01abe1a47894c1fbfc35c3a3af804ef Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Wed, 30 Jul 2014 09:54:46 +0200 Subject: The heater example is not a very good example... --- doc/readme.pdf | Bin 263736 -> 276546 bytes doc/readme.tm | 111 ++++++++++++++++++++++++++++++++++++++++--------------- doc/research.bib | 70 +++++++++++++++++++++++++++++++++++ 3 files changed, 151 insertions(+), 30 deletions(-) create mode 100644 doc/research.bib (limited to 'doc') diff --git a/doc/readme.pdf b/doc/readme.pdf index 89e5d4e..4c2482c 100644 Binary files a/doc/readme.pdf and b/doc/readme.pdf 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> Preuve de propriétés de sûreté sur des programmes @@ -17,6 +17,10 @@ Étude d'intervalles de variation pour des variables + Nos travaux se placent dans la continuité de , + , , , + . + 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) + \; + 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. + \; + @@ -1111,8 +1119,8 @@ Étant donné notre système représenté par une fonction de transition > et une fonction de cycle > (par facilité, on notera =c\f>), l'ensemble des - états accessible par le système est =lfp>s.I\g|)>>, - où =|i|\>|)>>. + états accessible par le système est =lfp>s.S\g|)>>, + où =|i|\>|)>>. Pour \\>, notons > : \\\> @@ -1125,7 +1133,7 @@ Poser : <\eqnarray*> - >||>>|>||\\| + >||>>|>||\\| s\\|}>>>>> @@ -1150,7 +1158,7 @@ et non par union simple dans le futur. La définition devient alors : <\eqnarray*> - >||>>|>||\\| + >||>>|>||\\| s\\|}>>>|,0>>||>>>> @@ -1175,7 +1183,7 @@ d'itération suivant : <\eqnarray*> - >||>>|>||\\| + >||>>|>||\\| s\\|}>>>|,0>>||>>>> @@ -1407,7 +1415,7 @@ <\eqnarray*> >||> - I>>>> + S>>>> (appliquer > de la sorte permet de faire que toutes les @@ -1445,9 +1453,9 @@ - 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 + Une autre approche à base de partitionnement dynamique a été tentée (cette + approche est décrite dans ), 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> - parser, lexer, typeur pour notre sous-ensemble de SCADE (source des - fichiers dans ) + lexer, parser, typeur symple pour notre sous-ensemble de SCADE + (source des fichiers dans ) - interprète pour la sémantique cocnrète + interprète pour la sémantique concrète () 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> - , , International Symposium on Static Analysis, SAS'94. - - , and , - , IEEE Transactions on - Software Engineering, Spcial Issue on the Specification and Analysis of - Real-Time Systems, Sept. 1992 - - , and , - , Static - Analysis Symposium, SAS'99. - + <\bibliography|bib|tm-plain|research.bib> + <\bib-list|5> + B.Blanchet, + P.Cousot, R.Cousot, J.Feret, L.Mauborgne, + A.Miné, D.MonniauxX.Rival. + A static analyzer for large safety-critical software. + , 196--207. San Diego, California, USA, June + 7--14 2003. ACM Press. + + P.CousotR.Cousot. Systematic design of program analysis + frameworks. , 269--282. San Antonio, + Texas, 1979. ACM Press, New York, NY. + + N.Halbwachs. About + synchronous programming and abstract interpretation. + B.LeCharlier, + . Namur (belgium), September 1994. LNCS 864, Springer + Verlag. + + N.Halbwachs, + F.LagnierC.Ratel. Programming and + verifying real-time systems by means of the synchronous data-flow + programming language lustre. , , September + \ 1992. + + B.Jeannet, + N.HalbwachsP.Raymond. Dynamic + partitioning in analyses of numerical properties. + . Venezia (Italy), sep 1999. + + \; @@ -1813,15 +1845,34 @@ > > |\>|20>> + > > > > > + > + > + > + > + > <\auxiliary> <\collection> + <\associate|bib> + blanchetEtAl-PLDI03 + + cousotCousot79-1 + + halbwachs94c + + lesartse + + jhrsas99 + + jhrsas99 + <\associate|toc> |math-font-series||1Introduction> |.>>>>|> @@ -2025,7 +2076,7 @@ taille réelle \T |.>>>>|> > - |math-font-series||Références> + |math-font-series||Bibliographie> |.>>>>|> 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, +} -- cgit v1.2.3