Changeset 64

Timestamp:

Mar 14, 2012, 1:43:13 PM (13 years ago)

Author:

syed

Message:

/papers/FDL2012/

Location:

papers/FDL2012

Files:

• FDL2012.tex (modified) (4 diffs)
• exp_results.tex (added)
• myBib.bib (modified) (9 diffs)

papers/FDL2012/FDL2012.tex

@@ -29 +29 @@
 \newcommand{\remark}[2]{\textcolor{blue}{#1: #2}}
 
-\graphicspath{{schema/}}
 
  \title{ Compositional System Verification: Exploiting components' verified properties in the abstraction-refinement process}
@@ -74 +73 @@
 \section{Experimental results}
 
- Work in progress... \\
+ \input{exp_results}
 
 
@@ -85 +84 @@
 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 +99 @@
 
 
-\end{document}
+\end{document} 

papers/FDL2012/myBib.bib

@@ -43 +43 @@
    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 +86 @@
     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 +143 @@
    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 +154 @@
    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 +160 @@
 
 @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 +184 @@
    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 +207 @@
    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 +283 @@
 }
 
-@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 +311 @@
 }
 
-@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,