Changeset 51 for biblio/biblio.bib

Timestamp:

Mar 7, 2012, 11:42:59 AM (13 years ago)

Author:

cecile

Message:

new articles for components based abstraction and compostion added

File:

• biblio/biblio.bib (modified) (11 diffs)

biblio/biblio.bib

@@ -448 +448 @@
   bibsource = {DBLP, http://dblp.uni-trier.de},
   crossref = {DBLP:conf/cav/2002},
-  ee = {http://link.springer.de/link/service/series/0558/bibs/2404/24040137.htm}
+  ee = {http://link.springer.de/link/service/series/0558/bibs/2404/24040137.htm},
+  keywords = {Abstraction}
 }
 
@@ -1330 +1331 @@
   year = {2007},
   note = {accepted},
+  keywords = {Abstraction, CEGAR, CTL},
   owner = {cecile},
   timestamp = {2007.03.27}
@@ -1481 +1483 @@
   pages = {1686-1691},
   file = {:Composition/Speeding up MC by exploiting Explicit09.PDF:PDF},
+  keywords = {Composition , model checking},
   owner = {cecile},
   timestamp = {2009.04.30}
@@ -1788 +1791 @@
 }
 
+@INPROCEEDINGS{6128043,
+  author = {Yuzhang Feng and Veeramani, A. and Kanagasabai, R. and Seungmin Rho},
+  title = {Automatic Service Composition via Model Checking},
+  booktitle = {Services Computing Conference (APSCC), 2011 IEEE Asia-Pacific},
+  year = {2011},
+  pages = {477 -482},
+  month = {dec.},
+  abstract = {Web service composition is the process of constructing a set of Web
+        services which, when invoked with some user input in a particular
+        order, can produce the output to the user's requirements. This paper
+        proposes a novel model checking based approach for automated service
+        composition. Modeling services as a set of interleaved processes
+        in a class of process algebra, we formulate service composition as
+        model checking asserted on a specific type of property on the model.
+        We show that, under this formulation, correct composition workflows
+        can be constructed from the counter-examples provided by model checking.
+        With a case study on online hotel booking services, we demonstrate
+        that the proposed approach can support directed a cyclic composition
+        graphs and the generated composition graphs are automatically verified.},
+  doi = {10.1109/APSCC.2011.54},
+  file = {:/users/outil/verif/biblio/Composition/AutomaticServiceCompositionViaModelChecking2011.pdf:PDF},
+  keywords = {Web service composition;automated service composition;directed acyclic
+        composition graph;interleaved process;model checking;online hotel
+        booking services;process algebra;user requirements;Web services;directed
+        graphs;formal verification;hotel industry;process algebra;},
+  owner = {cecile},
+  timestamp = {2012.03.07}
+}
+
 @ARTICLE{DBLP:journals/tcad/FeySBD08,
   author = {G{\"o}rschwin Fey and Stefan Staber and Roderick Bloem and Rolf Drechsler},
@@ -2202 +2234 @@
 }
 
+@INCOLLECTION{springerlink:10.1007/978-3-540-68073-4_4,
+  author = {Li, Juncao and Sun, Xiuli and Xie, Fei and Song, Xiaoyu},
+  title = {Component-Based Abstraction and Refinement},
+  booktitle = {High Confidence Software Reuse in Large Systems},
+  publisher = {Springer Berlin / Heidelberg},
+  year = {2008},
+  editor = {Mei, Hong},
+  volume = {5030},
+  series = {Lecture Notes in Computer Science},
+  pages = {39-51},
+  note = {10.1007/978-3},
+  affiliation = {Portland State University Dept. of Computer Science Portland OR 97207},
+  file = {:/users/outil/verif/biblio/Composition/Compponent-Based AbstractionRefinement2008.pdf:PDF},
+  isbn = {978-3-540-68062-8},
+  keyword = {Computer Science},
+  keywords = {Composition, Abstraction, Refinement, verified component, Hardware/software
+        coverification},
+  url = {http://dx.doi.org/10.1007/978-3-540-68073-4_4}
+}
+
 @INPROCEEDINGS{lin91implicit,
   author = {B.~Lin and A.R.~Newton},
@@ -2226 +2278 @@
   address = {Hingham, MA, USA},
   publisher = {Kluwer Academic Publisher}
+}
+
+@INCOLLECTION{springerlink:10.1007/978-3-642-16901-4_15,
+  author = {Lomuscio, Alessio and Strulo, Ben and Walker, Nigel and Wu, Peng},
+  title = {Assume-Guarantee Reasoning with Local Specifications},
+  booktitle = {Formal Methods and Software Engineering},
+  publisher = {Springer Berlin / Heidelberg},
+  year = {2010},
+  editor = {Dong, Jin and Zhu, Huibiao},
+  volume = {6447},
+  series = {Lecture Notes in Computer Science},
+  pages = {204-219},
+  note = {10.1007/978-3-642-16901-4_15},
+  abstract = {We investigate assume-guarantee reasoning for global specifications
+        consisting of conjunctions of local specifications. We present a
+        sound and complete assume-guarantee rule that permits reasoning about
+        individual modules for local specifications and draws conclusions
+        on global specifications. We illustrate our approach with an example
+        from the field of network congestion control, where different agents
+        are responsible for controlling packet flow across a shared infrastructure.
+        In this context, we derive an assume-guarantee rule for system stability,
+        and show that this rule is valuable to reason about any number of
+        agents, any initial flow configuration, and any topology of bounded
+        degree.},
+  affiliation = {Department of Computing, Imperial College London, UK},
+  file = {:/users/outil/verif/biblio/Composition/AGRwithLocalSpecification2010.pdf:PDF},
+  isbn = {978-3-642-16900-7},
+  keyword = {Computer Science},
+  keywords = {Compositional reasoning, composition},
+  owner = {cecile},
+  timestamp = {2012.03.07},
+  url = {http://dx.doi.org/10.1007/978-3-642-16901-4_15}
 }
 
@@ -2448 +2532 @@
   pages = {2-14},
   number = {1},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
+  bibsource = {DBLP, http://dblp.uni-trier.de},
+  keywords = {Abstraction}
 }
 
@@ -2559 +2644 @@
   publisher = {Springer-Verlag},
   url = {http://www.csl.sri.com/papers/cade92-pvs/}
+}
+
+@INCOLLECTION{springerlink:10.1007/3-540-63166-6_5,
+  author = {Pardo, Abelardo and Hachtel, Gary},
+  title = {Automatic abstraction techniques for propositional $\mu$-calculus
+        model checking},
+  booktitle = {Computer Aided Verification},
+  publisher = {Springer Berlin / Heidelberg},
+  year = {1997},
+  editor = {Grumberg, Orna},
+  volume = {1254},
+  series = {Lecture Notes in Computer Science},
+  pages = {12-23},
+  note = {10.1007/3-540-63166-6_5},
+  abstract = {An abstraction/refinement paradigm for the full propositional $\mu$-calculus
+        is presented. No distinction is made between universal or existential
+        fragments. Necessary conditions for conservative verification are
+        provided, along with a fully automatic symbolic model checking abstraction
+        algorithm. The algorithm begins with conservative verification of
+        an initial abstraction. If the conclusion is negative, it derives
+        a ldquogoal setrdquo of states which require further resolution.
+        It then successively refines, with respect to this goal set, the
+        approximations made in the subformulas, until the given formula is
+        verified or computational resources are exhausted.},
+  affiliation = {University of Colorado ECEN Campus Box 425 80309 Boulder CO USA ECEN
+        Campus Box 425 80309 Boulder CO USA},
+  file = {:/users/outil/verif/biblio/Cegar/CAV97_Automatic_Abstraction_Tech_for_Propositional_uCalc_MC.ps:PostScript},
+  isbn = {978-3-540-63166-8},
+  keywords = {Computer Science, Abstraction, model checking, mu-calculus, refinement},
+  owner = {cecile},
+  timestamp = {2012.03.07},
+  url = {http://dx.doi.org/10.1007/3-540-63166-6_5}
+}
+
+@INPROCEEDINGS{Pardo:1998:ICM:277044.277171,
+  author = {Pardo, Abelardo and Hachtel, Gary D.},
+  title = {Incremental CTL model checking using BDD subsetting},
+  booktitle = {Proceedings of the 35th annual Design Automation Conference},
+  year = {1998},
+  series = {DAC '98},
+  pages = {457--462},
+  address = {New York, NY, USA},
+  publisher = {ACM},
+  abstract = {An automatic abstraction/refinement algorithm for symbolic CTL model
+        checking is presented. Conservative model checking is thus done for
+        the full CTL language-no restriction is made to the universal or
+        existen tial fragments. The algorithm begins with conserv ativ everification
+        of an initial abstraction. If the conclusion is negativ e,it deriv
+        es a ¿goal set¿ of states which require further resolution. It then
+        successiv ely refines, with respect to this goal set, the appro ximations
+        made in the sub-formulas, until the giv en form ula is v erified
+        or computational resources are exhausted. This method applies uniformly
+        to the abstractions based in over-appro ximation as well as under-approximations
+        of the model. Both the refinement and the abstraction procedures
+        are based in BDD-subsetting. Note that refinement procedures which
+        are based on error traces, are limited to over-appro ximation on
+        the universal fragment (or for language con tainment), whereas the
+        goal set method is applicable to all consisten t appro ximations,
+        and for all CTL formulas.},
+  acmid = {277171},
+  doi = {10.1145/277044.277171},
+  file = {:/users/outil/verif/biblio/Cegar/DAC98_Incremental CTL Model Checking Using BDD Subsetting.pdf:PDF},
+  isbn = {0-89791-964-5},
+  keywords = {CTL, model checking, Abstraction},
+  location = {San Francisco, California, United States},
+  numpages = {6},
+  url = {http://doi.acm.org/10.1145/277044.277171}
 }
 
@@ -2874 +3026 @@
   publisher = {IEEE Computer Society},
   doi = {http://dx.doi.org/10.1109/LICS.2006.5},
+  keywords = {Abstraction, 3-valued},
   owner = {cecile},
   timestamp = {2007.01.14}
@@ -2935 +3088 @@
   owner = {cecile},
   timestamp = {2006.02.09}
+}
+
+@INPROCEEDINGS{Tripakis201,
+  author = {Tripakis, Stavros and Andrade, Hugo and Ghosal, Arkadeb and Limaye,
+        Rhishikesh and Ravindran, Kaushik and Wang, Guoqiang and Yang, Guang
+        and Kormerup, Jacob and Wong, Ian},
+  title = {Correct and non-defensive glue design using abstract models},
+  booktitle = {Proceedings of the seventh IEEE/ACM/IFIP international conference
+        on Hardware/software codesign and system synthesis},
+  year = {2011},
+  series = {CODES+ISSS '11},
+  pages = {59--68},
+  address = {New York, NY, USA},
+  publisher = {ACM},
+  abstract = { Current hardware design practice often relies on integration of components,
+        some of which may be IP or legacy blocks. While integration eases
+        design by allowing modularization and component reuse, it is still
+        done in a mostly ad hoc manner. Designers work with descriptions
+        of components that are either informal or incomplete (e.g., documents
+        in English, structural but non-behavioral specifications in IP-XACT)
+        or too low-level (e.g., HDL code), and have little to no automatic
+        support for stitching the components together. Providing such support
+        is the glue design problem.
+        
+        This paper addresses this problem using a model-based approach. The
+        key idea is to use high-level models, such as dataflow graphs, that
+        enable efficient automated analysis. The analysis can be used to
+        derive performance properties of the system (e.g., component compatibility,
+        throughput, etc.), optimize resource usage (e.g., buffer sizes),
+        and even synthesize low-level code (e.g., control logic). However,
+        these models are only abstractions of the real system, and often
+        omit critical information. As a result, the analysis outcomes may
+        be defensive (e.g., buffers that are too big) or even incorrect (e.g.,
+        buffers that are too small). The paper examines these situations
+        and proposes a correct and non-defensive design methodology that
+        employs the right models to explore accurate performance and resource
+        trade-offs. },
+  acmid = {2039382},
+  doi = {http://doi.acm.org/10.1145/2039370.2039382},
+  isbn = {978-1-4503-0715-4},
+  keywords = {abstraction, data flow, glue design, non-defensiveness, composition},
+  location = {Taipei, Taiwan},
+  numpages = {10},
+  owner = {cecile},
+  timestamp = {2012.03.07},
+  url = {http://doi.acm.org/10.1145/2039370.2039382}
 }
 
@@ -3029 +3228 @@
 }
 
+@ARTICLE{5374376,
+  author = {Hao Zheng and Haiqiong Yao and Yoneda, T.},
+  title = {Modular Model Checking of Large Asynchronous Designs with Efficient
+        Abstraction Refinement},
+  journal = {Computers, IEEE Transactions on},
+  year = {2010},
+  volume = {59},
+  pages = {561 -573},
+  number = {4},
+  month = {april },
+  abstract = {Divide-and-conquer is essential to address state explosion in model
+        checking. Verifying each individual component in a system, in isolation,
+        efficiently requires an appropriate context, which traditionally
+        is obtained by hand. This paper presents an efficient modular model
+        checking approach for asynchronous design verification. It is equipped
+        with a novel abstraction refinement method that can refine a component
+        abstraction to be accurate enough for successful verification. It
+        is fully automated, and eliminates the need of finding an accurate
+        context when verifying each individual component, although such a
+        context is still highly desirable. This method is also enhanced with
+        additional state space reduction techniques. The experiments on several
+        nontrivial asynchronous designs show that this method efficiently
+        removes impossible behaviors from each component including ones violating
+        correctness requirements.},
+  doi = {10.1109/TC.2009.187},
+  file = {:/users/outil/verif/biblio/Composition/ModularMCLargeAsynchronousDesignwithAR2010.pdf:PDF},
+  issn = {0018-9340},
+  keywords = {abstraction refinement;abstraction refinement method;large asynchronous
+        designs;modular model checking;state explosion;state space reduction
+        techniques;formal verification;state-space methods; composition},
+  owner = {cecile},
+  review = {Verification of a whole system by verifying each components. When
+        verifying each components individually assumptions has to be made
+        on the environnment ot avoid false counter-examples. Use component
+        abstraction to over-approximated the environment. This abastraction
+        must be refined to obtain only the behavior allowed at the interface.
+        They propose : 
+        
+        <ul>
+        
+        <li>     to identify and remove unsynchronized behavior. 
+        
+         <li> to extend the refinement to more than two components itemize
+        
+        
+        </ul>
+        
+        
+        Main contribution : Local synchronization detection method for component
+        based on parallel composition and an AR methof for modular MC.
+        
+        <br>
+        
+        Circuit class : Asynchronous</td>},
+  timestamp = {2012.03.07}
+}
+
 @PROCEEDINGS{DBLP:conf/fmcad/2002,
   title = {Formal Methods in Computer-Aided Design, 4th International Conference,