Changeset 64


Ignore:
Timestamp:
Mar 14, 2012, 1:43:13 PM (13 years ago)
Author:
syed
Message:

/papers/FDL2012/

Location:
papers/FDL2012
Files:
1 added
2 edited

Legend:

Unmodified
Added
Removed
  • papers/FDL2012/FDL2012.tex

    r63 r64  
    2929\newcommand{\remark}[2]{\textcolor{blue}{#1: #2}}
    3030
    31 \graphicspath{{schema/}}
    3231
    3332 \title{ Compositional System Verification: Exploiting components' verified properties in the abstraction-refinement process}
     
    7473\section{Experimental results}
    7574
    76  Work in progress... \\
     75 \input{exp_results}
    7776
    7877
     
    8584We 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.
    8685
    87 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.
     86Nevertheless, 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.
    8887
    8988
     
    10099
    101100
    102 \end{document}
     101\end{document} 
  • papers/FDL2012/myBib.bib

    r62 r64  
    4343   author = "E. M. Clarke and  O. Grumberg and S. Jha and Y. Lu and H. Veith",
    4444   title = "{Counterexample-guided Abstraction Refinement}",
    45    booktitle = "Computer Aided Verification (CAV'00)",
     45   booktitle = "Computer Aided Verification (CAV '00)",
    4646   address = "Chicago, IL",
    4747   year = 2000,
     
    8686    author = "H. S. Jin and M. Awedh and F. Somenzi",
    8787    title = "{CirCUs: A Satisfiablilty Solver Geared Towards Bounded Model Checking}",
    88      booktitle = {16th Conference on Computer Aided Verification (CAV'04)},
     88     booktitle = {16th Conference on Computer Aided Verification (CAV '04)},
    8989    pages = {519-522},
    9090    year = 2004,
     
    143143   author = "H. Peng and Y. Mokhtari and S. Tahar ",
    144144   title = "{Environment Synthesis for Compositional Model Checking} ",
    145    booktitle = "In ICCD'02 : Proceedings of the 20th International Conference on Computer Design",
     145   booktitle = "In ICCD’02 : Proceedings of the 20th International Conference on Computer Design",
    146146   pages = {70-75},
    147147   address = "Freiburg, Germany",
     
    154154   author = "M. Schickel  and V. Nimbler and M. Braun and H. Eveking ",
    155155   title = "{On Consistency and Completeness of Property-Sets: Exploiting the Property-Based Design Process} ",
    156    booktitle = "In FDL'06: Proceedings of  Forum on specification and Design Languages",
     156   booktitle = "In FDL’06: Proceedings of  Forum on specification and Design Languages",
    157157   year = 2006
    158158}
     
    160160
    161161@conference{ CiardoLS00mdd_async,
    162    author = "G.Ciardo and G. LÌttgen and R. Siminiceanu",
     162   author = "G.Ciardo and G. LÃŒttgen and R. Siminiceanu",
    163163   title = "{ Efficient symbolic state-space construction for asynchronous systems} ",
    164164   booktitle = "In Proc. of ICATPN '2000",
     
    184184   author = "T. A. Henzinger and S. Qadeer and S. K. Rajamani",
    185185   title = "{ You Assume, We Guarantee : Methodology and Case Studies} ",
    186    booktitle = "CAV'98 : Proceedings of the 10th International Conference on Computer Aided Verification",
     186   booktitle = "CAV â€™98 : Proceedings of the 10th International Conference on Computer Aided Verification",
    187187   volume = 1427,
    188188   pages = {440-451},
     
    207207   author = "  S. Graf and H. Saïdi",
    208208   title = "{ Construction of Abstract State Graphs with PVS} ",
    209    booktitle = " In CAV'97: Proceedings of the 9th International Conference on Computer Aided Verification",
     209   booktitle = " In CAV â€™97: Proceedings of the 9th International Conference on Computer Aided Verification",
    210210   volume = 1254,
    211211   year = 1997,
    212212   publisher = " Lecture Notes in Computer Science, Springer"
     213}
     214
     215
     216
     217@conference{ PardoHachtel97autoAbsMC,
     218   author = "  S. Pardo and G. Hachtel",
     219   title = "{ Automatic Abstraction Technique for Propositional mu-Calculus Model Checking} ",
     220   booktitle = " In CAV ’97: Proceedings of the 9th International Conference on Computer Aided Verification",
     221   volume = 1254,
     222   pages = {12-23},
     223   year = 1997,
     224   publisher = " Lecture Notes in Computer Science, Springer-Verlag"
     225}
     226
     227
     228@conference{ PardoHachtel98incremCTLMC,
     229   author = "  S. Pardo and G. Hachtel",
     230   title = "{ Incremental CTL Model Checking Using BDD Subsetting} ",
     231   booktitle = " In DAC ’98: 35th Design Automation Conference ",
     232   pages = {457-462},
     233   year = 1998,
    213234}
    214235
     
    262283}
    263284
    264 @ARTICLE{clarke94model,
    265   author = {E.M.~Clarke and O.~Grumberg and D.E.~Long},
    266   title = {{Model Checking and Abstraction}},
    267   journal = {ACM Transactions on Programming Languages and Systems},
    268   year = {1994},
    269   volume = {16},
    270   pages = {1512--1542},
    271   number = {5},
    272   address = {New York, NY, USA},
    273   doi = {http://doi.acm.org/10.1145/186025.186051},
    274   issn = {0164-0925},
    275   keywords = {model cheking, abstraction, CTL, preservation},
    276   publisher = {ACM Press}
    277 }
    278285
    279286@inproceedings{pwk2009-date,
     
    304311}
    305312
    306 @PHDTHESIS{braunstein_phd07,
    307   author = {C.~Braunstein},
    308   title = {"Conception Incrémentale, Vérification de Composants Matériels et
    309         Méthode d'abstraction pour la Vérification de SystÚmes Intégrés sur
    310         Puce"},
    311   school = {{Universitée Pierre et Marie Curie (Paris 6)}},
    312   year = {2007},
    313   address = {LIP6/SOC},
    314   owner = {cecile},
    315   timestamp = {2007.04.16}
    316 }
    317313
    318314@misc{ patanshnik88bibtex,
Note: See TracChangeset for help on using the changeset viewer.