Index: papers/FDL2012/FDL2012.tex
===================================================================
--- papers/FDL2012/FDL2012.tex	(revision 63)
+++ papers/FDL2012/FDL2012.tex	(revision 64)
@@ -29,5 +29,4 @@
 \newcommand{\remark}[2]{\textcolor{blue}{#1: #2}}
 
-\graphicspath{{schema/}}
 
  \title{ Compositional System Verification: Exploiting components' verified properties in the abstraction-refinement process}
@@ -74,5 +73,5 @@
 \section{Experimental results}
 
- Work in progress... \\
+ \input{exp_results}
 
 
@@ -85,5 +84,5 @@
 We have presented a new strategy in the abstraction generation and refinement which is well adapted for compositional embedded systems. This verification technique is compatible and suits well in the natural development process of complex systems. Our preliminary experimental results shows an interesting performance in terms duration of abstraction generation and the number of refinement iteration. Futhermore, this technique enables us to overcome repetitive counterexamples due to the presence of cycles in the system's graph.
 
-Nevertheless, in order to function well, this refinement technique requires a complete specification of every components of the concrete model. Furthermore, it may be possible that none of the properties available is capable of eliminating the counterexample which probably due to the fact that the specification is not complete or counterexample given is provoked by the composition of components. In this case, other refinement techniques such as the refinement by eliminating the counterexample only techniques should be considered. We are currently investigating other complementary techniques to overcome these particular cases.
+Nevertheless, in order to function well, this refinement technique requires a complete specification of every components of the concrete model. Futhermore, it may be possible that none of the properties available is capable of eliminating the counterexample which probably due to the fact that the specification is not complete or counterexample given is provoqued by the composition of components. In this case, other refinement techniques such as the refinement by eliminating the counterexample only techniques should be considered. We are currently investigating other complementary techniques to overcome these particular cases.
 
 
@@ -100,3 +99,3 @@
 
 
-\end{document}
+\end{document} 
Index: papers/FDL2012/exp_results.tex
===================================================================
--- papers/FDL2012/exp_results.tex	(revision 64)
+++ papers/FDL2012/exp_results.tex	(revision 64)
@@ -0,0 +1,62 @@
+We have conducted preliminary experiments to tests and compare the performance of our strategy with existing abstraction-refinement technique available in VIS. As our abstraction representation requires fairness constraints, we have chosen the \emph{incremental\_ctl\_verification} abstraction refinement technique as it supports CTL formulas and fairness constraints \cite{PardoHachtel98incremCTLMC} \cite{PardoHachtel97autoAbsMC}. 
+
+
+We have executed and compared the execution time and the number of refinement iterations for two examples: VCI-PI platform consisting of Virtual Component Interface (VCI), a PI-Bus and VCI-PI protocol converter and a simplified version of a CAN bus platform consisting of 3 nodes and a CAN bus. The results have been obtained on a PC with an AMD Athlon dual-core processor 4450e and 1.8GB of RAM memory.
+
+
+\medskip
+
+\begin{table} [h]
+%\hspace*{-8mm}
+\begin{tabular}{|c|c|c|c|}
+
+\toprule 
+\textbf{VCI} & \emph{Verification} & \emph{Verification}  & \emph{Refinement} \\ 
+ \textbf{-PI}& \emph{Technique}  & \emph{Time (s)}       & \emph{Iteration} \\
+\midrule
+\midrule
+ 	     & Prop. Selection &    2.2    & 1 \\
+ $\phi_1$   & Incremental      &  18.1    & 0    \\
+ 	     & Standard MC    &  14.9    & - \\
+\midrule
+ 	     & Prop\_Selection &     1.0    & 0 \\
+ $\phi_2$   & Incremental      & 168.0    & 467    \\
+ 	     & Standard MC    &   14.9    & - \\
+\bottomrule
+
+\end{tabular}
+ 
+\caption{\label{TabVCI_PI} Results on VCI-PI platform }
+\end{table}
+
+%\medskip
+
+\begin{table} [h]
+%\hspace*{-8mm}
+\begin{tabular}{|c|c|c|c|}
+
+\toprule 
+\textbf{CAN} & \emph{Verification} & \emph{Verification}  & \emph{Refinement} \\ 
+\textbf{Bus}  & \emph{Technique}  & \emph{Time (s)}       & \emph{Iteration} \\
+\midrule
+\midrule
+ 	      & Prop. Selection  &             &       \\
+ $\phi_1$   & Incremental       &  >1 day  & 0    \\
+ 	      & Standard MC     &  51.9    & - \\
+\midrule
+ 	     & Prop\_Selection &              &   \\
+ $\phi_2$   & Incremental      &   57.3    & 0   \\
+ 	     & Standard MC     &     2.2    & - \\
+\bottomrule
+
+\end{tabular}
+ 
+\caption{\label{TabCANBus} Results on CAN Bus platform }
+\end{table}
+
+\medskip
+
+Table 1 shows the... 
+\TODO{Comments about Table 1, Table 2 and conclusion of Experimental Results} 
+
+
Index: papers/FDL2012/myBib.bib
===================================================================
--- papers/FDL2012/myBib.bib	(revision 63)
+++ papers/FDL2012/myBib.bib	(revision 64)
@@ -43,5 +43,5 @@
    author = "E. M. Clarke and  O. Grumberg and S. Jha and Y. Lu and H. Veith",
    title = "{Counterexample-guided Abstraction Refinement}",
-   booktitle = "Computer Aided Verification (CAV'00)",
+   booktitle = "Computer Aided Verification (CAV '00)",
    address = "Chicago, IL",
    year = 2000,
@@ -86,5 +86,5 @@
     author = "H. S. Jin and M. Awedh and F. Somenzi",
     title = "{CirCUs: A Satisfiablilty Solver Geared Towards Bounded Model Checking}",
-     booktitle = {16th Conference on Computer Aided Verification (CAV'04)},
+     booktitle = {16th Conference on Computer Aided Verification (CAV '04)},
     pages = {519-522},
     year = 2004,
@@ -143,5 +143,5 @@
    author = "H. Peng and Y. Mokhtari and S. Tahar ",
    title = "{Environment Synthesis for Compositional Model Checking} ",
-   booktitle = "In ICCD'02 : Proceedings of the 20th International Conference on Computer Design",
+   booktitle = "In ICCD’02 : Proceedings of the 20th International Conference on Computer Design",
    pages = {70-75},
    address = "Freiburg, Germany",
@@ -154,5 +154,5 @@
    author = "M. Schickel  and V. Nimbler and M. Braun and H. Eveking ",
    title = "{On Consistency and Completeness of Property-Sets: Exploiting the Property-Based Design Process} ",
-   booktitle = "In FDL'06: Proceedings of  Forum on specification and Design Languages",
+   booktitle = "In FDL’06: Proceedings of  Forum on specification and Design Languages",
    year = 2006
 }
@@ -160,5 +160,5 @@
 
 @conference{ CiardoLS00mdd_async,
-   author = "G.Ciardo and G. LÌttgen and R. Siminiceanu",
+   author = "G.Ciardo and G. LÃŒttgen and R. Siminiceanu",
    title = "{ Efficient symbolic state-space construction for asynchronous systems} ",
    booktitle = "In Proc. of ICATPN '2000",
@@ -184,5 +184,5 @@
    author = "T. A. Henzinger and S. Qadeer and S. K. Rajamani",
    title = "{ You Assume, We Guarantee : Methodology and Case Studies} ",
-   booktitle = "CAV'98 : Proceedings of the 10th International Conference on Computer Aided Verification",
+   booktitle = "CAV ’98 : Proceedings of the 10th International Conference on Computer Aided Verification",
    volume = 1427,
    pages = {440-451},
@@ -207,8 +207,29 @@
    author = "  S. Graf and H. Saïdi",
    title = "{ Construction of Abstract State Graphs with PVS} ",
-   booktitle = " In CAV'97: Proceedings of the 9th International Conference on Computer Aided Verification",
+   booktitle = " In CAV ’97: Proceedings of the 9th International Conference on Computer Aided Verification",
    volume = 1254,
    year = 1997,
    publisher = " Lecture Notes in Computer Science, Springer"
+}
+
+
+
+@conference{ PardoHachtel97autoAbsMC,
+   author = "  S. Pardo and G. Hachtel",
+   title = "{ Automatic Abstraction Technique for Propositional mu-Calculus Model Checking} ",
+   booktitle = " In CAV ’97: Proceedings of the 9th International Conference on Computer Aided Verification",
+   volume = 1254,
+   pages = {12-23},
+   year = 1997,
+   publisher = " Lecture Notes in Computer Science, Springer-Verlag"
+}
+
+
+@conference{ PardoHachtel98incremCTLMC,
+   author = "  S. Pardo and G. Hachtel",
+   title = "{ Incremental CTL Model Checking Using BDD Subsetting} ",
+   booktitle = " In DAC ’98: 35th Design Automation Conference ",
+   pages = {457-462},
+   year = 1998,
 }
 
@@ -262,18 +283,4 @@
 }
 
-@ARTICLE{clarke94model,
-  author = {E.M.~Clarke and O.~Grumberg and D.E.~Long},
-  title = {{Model Checking and Abstraction}},
-  journal = {ACM Transactions on Programming Languages and Systems},
-  year = {1994},
-  volume = {16},
-  pages = {1512--1542},
-  number = {5},
-  address = {New York, NY, USA},
-  doi = {http://doi.acm.org/10.1145/186025.186051},
-  issn = {0164-0925},
-  keywords = {model cheking, abstraction, CTL, preservation},
-  publisher = {ACM Press}
-}
 
 @inproceedings{pwk2009-date,
@@ -304,15 +311,4 @@
 }
 
-@PHDTHESIS{braunstein_phd07,
-  author = {C.~Braunstein},
-  title = {"Conception Incrémentale, Vérification de Composants Matériels et
-	Méthode d'abstraction pour la Vérification de SystÚmes Intégrés sur
-	Puce"},
-  school = {{Universitée Pierre et Marie Curie (Paris 6)}},
-  year = {2007},
-  address = {LIP6/SOC},
-  owner = {cecile},
-  timestamp = {2007.04.16}
-}
 
 @misc{ patanshnik88bibtex,