source: biblio/compositional.bib

Last change on this file was 51, checked in by cecile, 13 years ago

new articles for components based abstraction and compostion added

File size: 9.1 KB
Line 
1% This file was created with JabRef 2.5.
2% Encoding: UTF8
3
4@INPROCEEDINGS{Cabodi09Speeding,
5  author = {G. Cabodi and P. Camurati and L. Garcia and M. Murciano and S. Nocco
6        and S. Quer},
7  title = {Speeding up Model Checking by Exploiting Explicit and Hidden Verification
8        Constraints},
9  booktitle = {DATE '09: Proceedings of the conference on Design, Automation and
10        Test in Europe},
11  year = {2009},
12  pages = {1686-1691},
13  abstract = {Constraints represent a key component of state-
14       
15        of-the-art verification tools based on compositional approaches
16       
17        and assume–guarantee reasoning. In recent years, most of the
18       
19        research efforts on verification constraints have focused on
20       
21        defining formats and techniques to encode, or to synthesize,
22       
23        constraints starting from the specification of the design.
24       
25        In this paper, we analyze the impact of constraints on the
26       
27        performance of model checking tools, and we discuss how to
28       
29        effectively exploit them. We also introduce an approach to
30       
31        explicitly derive verification constraints hidden in the design
32       
33        and/or in the property under verification. Such constraints may
34       
35        simply come from true design constraints, embedded within the
36       
37        properties, or may be generated in the general effort to reduce or
38       
39        partition the state space. Experimental results show that, in both
40       
41        cases, we can reap benefits for the overall verification process
42       
43        in several hard-to-solve designs, where we obtain speed-ups of
44       
45        more than one order of magnitude.},
46  file = {:Composition/Speeding up MC by exploiting Explicit09.PDF:PDF},
47  owner = {cecile},
48  timestamp = {2009.04.30}
49}
50
51@INPROCEEDINGS{6128043,
52  author = {Yuzhang Feng and Veeramani, A. and Kanagasabai, R. and Seungmin Rho},
53  title = {Automatic Service Composition via Model Checking},
54  booktitle = {Services Computing Conference (APSCC), 2011 IEEE Asia-Pacific},
55  year = {2011},
56  pages = {477 -482},
57  month = {dec.},
58  abstract = {Web service composition is the process of constructing a set of Web
59        services which, when invoked with some user input in a particular
60        order, can produce the output to the user's requirements. This paper
61        proposes a novel model checking based approach for automated service
62        composition. Modeling services as a set of interleaved processes
63        in a class of process algebra, we formulate service composition as
64        model checking asserted on a specific type of property on the model.
65        We show that, under this formulation, correct composition workflows
66        can be constructed from the counter-examples provided by model checking.
67        With a case study on online hotel booking services, we demonstrate
68        that the proposed approach can support directed a cyclic composition
69        graphs and the generated composition graphs are automatically verified.},
70  doi = {10.1109/APSCC.2011.54},
71  file = {:/users/outil/verif/biblio/Composition/AutomaticServiceCompositionViaModelChecking2011.pdf:PDF},
72  keywords = {Web service composition;automated service composition;directed acyclic
73        composition graph;interleaved process;model checking;online hotel
74        booking services;process algebra;user requirements;Web services;directed
75        graphs;formal verification;hotel industry;process algebra;}
76}
77
78@INCOLLECTION{springerlink:10.1007/978-3-642-16901-4_15,
79  author = {Lomuscio, Alessio and Strulo, Ben and Walker, Nigel and Wu, Peng},
80  title = {Assume-Guarantee Reasoning with Local Specifications},
81  booktitle = {Formal Methods and Software Engineering},
82  publisher = {Springer Berlin / Heidelberg},
83  year = {2010},
84  editor = {Dong, Jin and Zhu, Huibiao},
85  volume = {6447},
86  series = {Lecture Notes in Computer Science},
87  pages = {204-219},
88  note = {10.1007/978-3-642-16901-4_15},
89  abstract = {We investigate assume-guarantee reasoning for global specifications
90        consisting of conjunctions of local specifications. We present a
91        sound and complete assume-guarantee rule that permits reasoning about
92        individual modules for local specifications and draws conclusions
93        on global specifications. We illustrate our approach with an example
94        from the field of network congestion control, where different agents
95        are responsible for controlling packet flow across a shared infrastructure.
96        In this context, we derive an assume-guarantee rule for system stability,
97        and show that this rule is valuable to reason about any number of
98        agents, any initial flow configuration, and any topology of bounded
99        degree.},
100  affiliation = {Department of Computing, Imperial College London, UK},
101  file = {:/users/outil/verif/biblio/Composition/AGRwithLocalSpecification2010.pdf:PDF},
102  isbn = {978-3-642-16900-7},
103  keyword = {Computer Science},
104  keywords = {Compositional reasoning},
105  url = {http://dx.doi.org/10.1007/978-3-642-16901-4_15}
106}
107
108@INPROCEEDINGS{Tripakis201,
109  author = {Tripakis, Stavros and Andrade, Hugo and Ghosal, Arkadeb and Limaye,
110        Rhishikesh and Ravindran, Kaushik and Wang, Guoqiang and Yang, Guang
111        and Kormerup, Jacob and Wong, Ian},
112  title = {Correct and non-defensive glue design using abstract models},
113  booktitle = {Proceedings of the seventh IEEE/ACM/IFIP international conference
114        on Hardware/software codesign and system synthesis},
115  year = {2011},
116  series = {CODES+ISSS '11},
117  pages = {59--68},
118  address = {New York, NY, USA},
119  publisher = {ACM},
120  abstract = { Current hardware design practice often relies on integration of components,
121        some of which may be IP or legacy blocks. While integration eases
122        design by allowing modularization and component reuse, it is still
123        done in a mostly ad hoc manner. Designers work with descriptions
124        of components that are either informal or incomplete (e.g., documents
125        in English, structural but non-behavioral specifications in IP-XACT)
126        or too low-level (e.g., HDL code), and have little to no automatic
127        support for stitching the components together. Providing such support
128        is the glue design problem.
129       
130        This paper addresses this problem using a model-based approach. The
131        key idea is to use high-level models, such as dataflow graphs, that
132        enable efficient automated analysis. The analysis can be used to
133        derive performance properties of the system (e.g., component compatibility,
134        throughput, etc.), optimize resource usage (e.g., buffer sizes),
135        and even synthesize low-level code (e.g., control logic). However,
136        these models are only abstractions of the real system, and often
137        omit critical information. As a result, the analysis outcomes may
138        be defensive (e.g., buffers that are too big) or even incorrect (e.g.,
139        buffers that are too small). The paper examines these situations
140        and proposes a correct and non-defensive design methodology that
141        employs the right models to explore accurate performance and resource
142        trade-offs. },
143  acmid = {2039382},
144  doi = {http://doi.acm.org/10.1145/2039370.2039382},
145  isbn = {978-1-4503-0715-4},
146  keywords = {abstraction, data flow, glue design, non-defensiveness, composition},
147  location = {Taipei, Taiwan},
148  numpages = {10},
149  url = {http://doi.acm.org/10.1145/2039370.2039382}
150}
151
152@ARTICLE{5374376,
153  author = {Hao Zheng and Haiqiong Yao and Yoneda, T.},
154  title = {Modular Model Checking of Large Asynchronous Designs with Efficient
155        Abstraction Refinement},
156  journal = {Computers, IEEE Transactions on},
157  year = {2010},
158  volume = {59},
159  pages = {561 -573},
160  number = {4},
161  month = {april },
162  abstract = {Divide-and-conquer is essential to address state explosion in model
163        checking. Verifying each individual component in a system, in isolation,
164        efficiently requires an appropriate context, which traditionally
165        is obtained by hand. This paper presents an efficient modular model
166        checking approach for asynchronous design verification. It is equipped
167        with a novel abstraction refinement method that can refine a component
168        abstraction to be accurate enough for successful verification. It
169        is fully automated, and eliminates the need of finding an accurate
170        context when verifying each individual component, although such a
171        context is still highly desirable. This method is also enhanced with
172        additional state space reduction techniques. The experiments on several
173        nontrivial asynchronous designs show that this method efficiently
174        removes impossible behaviors from each component including ones violating
175        correctness requirements.},
176  doi = {10.1109/TC.2009.187},
177  file = {:/users/outil/verif/biblio/Composition/ModularMCLargeAsynchronousDesignwithAR2010.pdf:PDF},
178  issn = {0018-9340},
179  keywords = {abstraction refinement;abstraction refinement method;large asynchronous
180        designs;modular model checking;state explosion;state space reduction
181        techniques;formal verification;state-space methods; composition},
182  review = {Verification of a whole system by verifying each components. When
183        verifying each components individually assumptions has to be made
184        on the environnment ot avoid false counter-examples. Use component
185        abstraction to over-approximated the environment. This abastraction
186        must be refined to obtain only the behavior allowed at the interface.
187        They propose : \begin{itemize} \item to identify and remove unsynchronized
188        behavior. \item to extend the refinement to more than two components
189        \end{itemize} Main contribution : Local synchronization detection
190        method for component based on parallel composition and an AR methof
191        for modular MC. Circuit class : Asynchronous}
192}
193
Note: See TracBrowser for help on using the repository browser.