source: biblio/compositional.bib

% This file was created with JabRef 2.5.
% Encoding: UTF8

@INPROCEEDINGS{Cabodi09Speeding,
  author = {G. Cabodi and P. Camurati and L. Garcia and M. Murciano and S. Nocco
        and S. Quer},
  title = {Speeding up Model Checking by Exploiting Explicit and Hidden Verification
        Constraints},
  booktitle = {DATE '09: Proceedings of the conference on Design, Automation and
        Test in Europe},
  year = {2009},
  pages = {1686-1691},
  abstract = {Constraints represent a key component of state-
        
        of-the-art verification tools based on compositional approaches
        
        and assume–guarantee reasoning. In recent years, most of the
        
        research efforts on verification constraints have focused on
        
        defining formats and techniques to encode, or to synthesize,
        
        constraints starting from the specification of the design.
        
        In this paper, we analyze the impact of constraints on the
        
        performance of model checking tools, and we discuss how to
        
        effectively exploit them. We also introduce an approach to
        
        explicitly derive verification constraints hidden in the design
        
        and/or in the property under verification. Such constraints may
        
        simply come from true design constraints, embedded within the
        
        properties, or may be generated in the general effort to reduce or
        
        partition the state space. Experimental results show that, in both
        
        cases, we can reap benefits for the overall verification process
        
        in several hard-to-solve designs, where we obtain speed-ups of
        
        more than one order of magnitude.},
  file = {:Composition/Speeding up MC by exploiting Explicit09.PDF:PDF},
  owner = {cecile},
  timestamp = {2009.04.30}
}

@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;}
}

@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},
  url = {http://dx.doi.org/10.1007/978-3-642-16901-4_15}
}

@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},
  url = {http://doi.acm.org/10.1145/2039370.2039382}
}

@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},
  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 : \begin{itemize} \item to identify and remove unsynchronized
        behavior. \item to extend the refinement to more than two components
        \end{itemize} Main contribution : Local synchronization detection
        method for component based on parallel composition and an AR methof
        for modular MC. Circuit class : Asynchronous}
}