Changes between Version 5 and Version 6 of CompositionalBiblio


Ignore:
Timestamp:
Mar 7, 2012, 11:47:01 AM (13 years ago)
Author:
cecile
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • CompositionalBiblio

    v5 v6  
    567567<thead><tr><th width="20%">Author</th><th width="30%">Title</th><th width="4%">Year</th><th width="30%">Journal/Proceedings</th><th width="7%">Reftype</th><th width="4%">DOI/URL</th></tr></thead>
    568568<tbody>
     569<tr id="alder06ticc" class="entry">
     570        <td>Adler, B., de Alfaro, L., da Silva, L.D., Faella, M., Legay, A., Raman, V. &amp; Roy, P.&nbsp;Thomas Ball and Robert B. Jones (Ed.)</td>
     571        <td>Ticc: A Tool for Interface Compatibility and Composition. <p class="infolinks">[<a href="javascript:toggleInfo('alder06ticc','bibtex')">BibTeX</a>]</p></td>
     572        <td>2006</td>
     573        <td><br/>Vol. 4144CAV'06: Proceedings of 18th International Conference of Computer Aided Verification, pp. 59-62&nbsp;</td>
     574        <td>inproceedings</td>
     575        <td>&nbsp;</td>
     576</tr>
     577<tr id="bib_alder06ticc" class="bibtex noshow">
     578<td colspan="7"><b>BibTeX</b>:
     579<pre>
     580@inproceedings{alder06ticc,
     581  author = {B.T.~Adler and L.~de Alfaro and L.~Dias da Silva and M.~Faella and A.~Legay and V.~Raman and P.~Roy},
     582  title = {Ticc: A Tool for Interface Compatibility and Composition.},
     583  booktitle = {CAV'06: Proceedings of 18th International Conference of Computer Aided Verification},
     584  year = {2006},
     585  volume = {4144},
     586  pages = {59-62}
     587}
     588</pre></td>
     589</tr>
     590<tr id="amla01assume" class="entry">
     591        <td>Amla, N., Emerson, E.A., Namjoshi, K.S. &amp; Trefler, R.J.&nbsp;</td>
     592        <td>Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams <p class="infolinks">[<a href="javascript:toggleInfo('amla01assume','bibtex')">BibTeX</a>]</p></td>
     593        <td>2001</td>
     594        <td>TACAS 2001: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 465-479&nbsp;</td>
     595        <td>inproceedings</td>
     596        <td>&nbsp;</td>
     597</tr>
     598<tr id="bib_amla01assume" class="bibtex noshow">
     599<td colspan="7"><b>BibTeX</b>:
     600<pre>
     601@inproceedings{amla01assume,
     602  author = {N.~Amla and E.~A.~Emerson and K.~S.~Namjoshi and R.~J.~Trefler},
     603  title = {Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams},
     604  booktitle = {TACAS 2001: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
     605  publisher = {Springer-Verlag},
     606  year = {2001},
     607  pages = {465--479}
     608}
     609</pre></td>
     610</tr>
    569611<tr id="Cabodi09Speeding" class="entry">
    570612        <td>Cabodi, G., Camurati, P., Garcia, L., Murciano, M., Nocco, S. &amp; Quer, S.&nbsp;</td>
    571         <td>Speeding up Model Checking by Exploiting Explicit and Hidden Verification Constraints <p class="infolinks">[<a href="javascript:toggleInfo('Cabodi09Speeding','abstract')">Abstract</a>] [<a href="javascript:toggleInfo('Cabodi09Speeding','bibtex')">BibTeX</a>]</p></td>
     613        <td>Speeding up Model Checking by Exploiting Explicit and Hidden Verification Constraints <p class="infolinks">[<a href="javascript:toggleInfo('Cabodi09Speeding','bibtex')">BibTeX</a>]</p></td>
    572614        <td>2009</td>
    573615        <td>DATE '09: Proceedings of the conference on Design, Automation and Test in Europe, pp. 1686-1691&nbsp;</td>
    574616        <td>inproceedings</td>
    575617        <td>&nbsp;</td>
    576 </tr>
    577 <tr id="abs_Cabodi09Speeding" class="abstract noshow">
    578         <td colspan="7"><b>Abstract</b>: Constraints represent a key component of state-<p>of-the-art verification tools based on compositional approaches<p>and assume–guarantee reasoning. In recent years, most of the<p>research efforts on verification constraints have focused on<p>defining formats and techniques to encode, or to synthesize,<p>constraints starting from the specification of the design.<p>In this paper, we analyze the impact of constraints on the<p>performance of model checking tools, and we discuss how to<p>effectively exploit them. We also introduce an approach to<p>explicitly derive verification constraints hidden in the design<p>and/or in the property under verification. Such constraints may<p>simply come from true design constraints, embedded within the<p>properties, or may be generated in the general effort to reduce or<p>partition the state space. Experimental results show that, in both<p>cases, we can reap benefits for the overall verification process<p>in several hard-to-solve designs, where we obtain speed-ups of<p>more than one order of magnitude.</td>
    579618</tr>
    580619<tr id="bib_Cabodi09Speeding" class="bibtex noshow">
    … …  
    587626  year = {2009},
    588627  pages = {1686-1691}
     628}
     629</pre></td>
     630</tr>
     631<tr id="Cansell2001AbstractionandRefinementofFeatures" class="entry">
     632        <td>Cansell, D. &amp; M&eacute;ry, D.&nbsp;S. Gilmore and M. Ryan (Ed.)</td>
     633        <td>Abstraction and Refinement of Features <p class="infolinks">[<a href="javascript:toggleInfo('Cansell2001AbstractionandRefinementofFeatures','abstract')">Abstract</a>] [<a href="javascript:toggleInfo('Cansell2001AbstractionandRefinementofFeatures','bibtex')">BibTeX</a>]</p></td>
     634        <td>2001</td>
     635        <td>Language Constructs for Designing Features, pp. 65-84&nbsp;</td>
     636        <td>incollection</td>
     637        <td>&nbsp;</td>
     638</tr>
     639<tr id="abs_Cansell2001AbstractionandRefinementofFeatures" class="abstract noshow">
     640        <td colspan="7"><b>Abstract</b>: The composition of services and features often leads to unwanted situations, because it is a non-monotonic operation over services and features. When a new service is added to an existing system, conditions have to be checked to ensure that the resulting system satisfies a list of required properties. Following the system approach of Abrial, we develop services and features in an incremental way and use refinement to model the composition of services and features. Proof obligations state the preservation or the non-preservation of properties, namely invariant or more generally safety properties. The method helps us in understanding when a service is interfering with another, and allows us to give multiple views of each service according to the level of its refinement. Finally, we validate our method with the Atelier B tool.</td>
     641</tr>
     642<tr id="bib_Cansell2001AbstractionandRefinementofFeatures" class="bibtex noshow">
     643<td colspan="7"><b>BibTeX</b>:
     644<pre>
     645@incollection{Cansell2001AbstractionandRefinementofFeatures,
     646  author = {D.~Cansell and D.~M&eacute;ry},
     647  title = {Abstraction and Refinement of Features},
     648  booktitle = {Language Constructs for Designing Features},
     649  publisher = {Springer-Verlag},
     650  year = {2001},
     651  pages = {65--84}
     652}
     653</pre></td>
     654</tr>
     655<tr id="DBLP:conf/lics/ClarkeLM89" class="entry">
     656        <td>Clarke, E.M., Long, D.E. &amp; McMillan, K.L.&nbsp;</td>
     657        <td>Compositional Model Checking <p class="infolinks">[<a href="javascript:toggleInfo('DBLP:conf/lics/ClarkeLM89','bibtex')">BibTeX</a>]</p></td>
     658        <td>1989</td>
     659        <td>LICS'89: Proceedings of the 4th Annual Symposium on Logic in Computer Science, pp. 353-362&nbsp;</td>
     660        <td>inproceedings</td>
     661        <td>&nbsp;</td>
     662</tr>
     663<tr id="bib_DBLP:conf/lics/ClarkeLM89" class="bibtex noshow">
     664<td colspan="7"><b>BibTeX</b>:
     665<pre>
     666@inproceedings{DBLP:conf/lics/ClarkeLM89,
     667  author = {E.~M.~Clarke and D.~E.~Long and K.~L.~McMillan},
     668  title = {Compositional Model Checking},
     669  booktitle = {LICS'89: Proceedings of the 4th Annual Symposium on Logic in Computer Science},
     670  publisher = {IEEE Computer Society},
     671  year = {1989},
     672  pages = {353-362}
     673}
     674</pre></td>
     675</tr>
     676<tr id="6128043" class="entry">
     677        <td>Feng, Y., Veeramani, A., Kanagasabai, R. &amp; Rho, S.&nbsp;</td>
     678        <td>Automatic Service Composition via Model Checking <p class="infolinks">[<a href="javascript:toggleInfo('6128043','abstract')">Abstract</a>] [<a href="javascript:toggleInfo('6128043','bibtex')">BibTeX</a>]</p></td>
     679        <td>2011</td>
     680        <td>Services Computing Conference (APSCC), 2011 IEEE Asia-Pacific, pp. 477 -482&nbsp;</td>
     681        <td>inproceedings</td>
     682        <td><a href="http://dx.doi.org/10.1109/APSCC.2011.54">DOI</a> &nbsp;</td>
     683</tr>
     684<tr id="abs_6128043" class="abstract noshow">
     685        <td colspan="7"><b>Abstract</b>: 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.</td>
     686</tr>
     687<tr id="bib_6128043" class="bibtex noshow">
     688<td colspan="7"><b>BibTeX</b>:
     689<pre>
     690@inproceedings{6128043,
     691  author = {Yuzhang Feng and Veeramani, A. and Kanagasabai, R. and Seungmin Rho},
     692  title = {Automatic Service Composition via Model Checking},
     693  booktitle = {Services Computing Conference (APSCC), 2011 IEEE Asia-Pacific},
     694  year = {2011},
     695  pages = {477 -482},
     696  doi = {http://dx.doi.org/10.1109/APSCC.2011.54}
     697}
     698</pre></td>
     699</tr>
     700<tr id="jhala01microarchi" class="entry">
     701        <td>Jhala, R. &amp; McMillan, K.&nbsp;Alain Finkel G&eacute;rard Berry, Hubert Comon (Ed.)</td>
     702        <td>Microarchitecture Verification by Compositional Model Checking. <p class="infolinks">[<a href="javascript:toggleInfo('jhala01microarchi','bibtex')">BibTeX</a>]</p></td>
     703        <td>2001</td>
     704        <td><br/>Vol. 2102CAV'01: Proceedings of the 13th International Conference on Computer Aided Verification, pp. 396-410&nbsp;</td>
     705        <td>inproceedings</td>
     706        <td>&nbsp;</td>
     707</tr>
     708<tr id="bib_jhala01microarchi" class="bibtex noshow">
     709<td colspan="7"><b>BibTeX</b>:
     710<pre>
     711@inproceedings{jhala01microarchi,
     712  author = {Jhala, R. and McMillan, K.L.},
     713  title = {Microarchitecture Verification by Compositional Model Checking.},
     714  booktitle = {CAV'01: Proceedings of the 13th International Conference on Computer Aided Verification},
     715  publisher = {Springer},
     716  year = {2001},
     717  volume = {2102},
     718  pages = {396-410}
     719}
     720</pre></td>
     721</tr>
     722<tr id="springerlink:10.1007/978-3-540-68073-4_4" class="entry">
     723        <td>Li, J., Sun, X., Xie, F. &amp; Song, X.&nbsp;Hong Mei (Ed.)</td>
     724        <td>Component-Based Abstraction and Refinement <p class="infolinks">[<a href="javascript:toggleInfo('springerlink:10.1007/978-3-540-68073-4_4','bibtex')">BibTeX</a>]</p></td>
     725        <td>2008</td>
     726        <td><br/>Vol. 5030High Confidence Software Reuse in Large Systems, pp. 39-51&nbsp;</td>
     727        <td>incollection</td>
     728        <td><a href="http://dx.doi.org/10.1007/978-3-540-68073-4_4">URL</a>&nbsp;</td>
     729</tr>
     730<tr id="bib_springerlink:10.1007/978-3-540-68073-4_4" class="bibtex noshow">
     731<td colspan="7"><b>BibTeX</b>:
     732<pre>
     733@incollection{springerlink:10.1007/978-3-540-68073-4_4,
     734  author = {Li, Juncao and Sun, Xiuli and Xie, Fei and Song, Xiaoyu},
     735  title = {Component-Based Abstraction and Refinement},
     736  booktitle = {High Confidence Software Reuse in Large Systems},
     737  publisher = {Springer Berlin / Heidelberg},
     738  year = {2008},
     739  volume = {5030},
     740  pages = {39-51},
     741  note = {10.1007/978-3},
     742  url = {http://dx.doi.org/10.1007/978-3-540-68073-4_4}
    589743}
    590744</pre></td>
    … …  
    617771</pre></td>
    618772</tr>
     773<tr id="long93thesis" class="entry">
     774        <td>Long, D.E.&nbsp;</td>
     775        <td>Model Checking, Abstraction, and Compositional Verification <p class="infolinks">[<a href="javascript:toggleInfo('long93thesis','bibtex')">BibTeX</a>]</p></td>
     776        <td>1993</td>
     777        <td><i>School</i>: Carnegie Mellon University&nbsp;</td>
     778        <td>phdthesis</td>
     779        <td>&nbsp;</td>
     780</tr>
     781<tr id="bib_long93thesis" class="bibtex noshow">
     782<td colspan="7"><b>BibTeX</b>:
     783<pre>
     784@phdthesis{long93thesis,
     785  author = {D.~E.~Long},
     786  title = {Model Checking, Abstraction, and Compositional Verification},
     787  school = {Carnegie Mellon University},
     788  year = {1993}
     789}
     790</pre></td>
     791</tr>
     792<tr id="mcmillan98tomasulo" class="entry">
     793        <td>McMillan, K.&nbsp;Moshe Y. Vardi Alan J. Hu (Ed.)</td>
     794        <td>Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking. <p class="infolinks">[<a href="javascript:toggleInfo('mcmillan98tomasulo','bibtex')">BibTeX</a>]</p></td>
     795        <td>1998</td>
     796        <td><br/>Vol. 1427CAV'98: Proceddings of the 10th International Conference on Computer Aided Verification, pp. 110-121&nbsp;</td>
     797        <td>inproceedings</td>
     798        <td>&nbsp;</td>
     799</tr>
     800<tr id="bib_mcmillan98tomasulo" class="bibtex noshow">
     801<td colspan="7"><b>BibTeX</b>:
     802<pre>
     803@inproceedings{mcmillan98tomasulo,
     804  author = {K.L.~McMillan},
     805  title = {Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking.},
     806  booktitle = {CAV'98: Proceddings of the 10th International Conference on Computer Aided Verification},
     807  publisher = {Springer},
     808  year = {1998},
     809  volume = {1427},
     810  pages = {110-121}
     811}
     812</pre></td>
     813</tr>
     814<tr id="mcmillan00methodology" class="entry">
     815        <td>McMillan, K.&nbsp;</td>
     816        <td>A Methodology for Hardware Verification Using Compositional Model Checking <p class="infolinks">[<a href="javascript:toggleInfo('mcmillan00methodology','bibtex')">BibTeX</a>]</p></td>
     817        <td>2000</td>
     818        <td>Science of Computer Programming<br/>Vol. 37(1-3), pp. 279-309&nbsp;</td>
     819        <td>article</td>
     820        <td><a href="citeseer.ist.psu.edu/mcmillan99methodology.html">URL</a>&nbsp;</td>
     821</tr>
     822<tr id="bib_mcmillan00methodology" class="bibtex noshow">
     823<td colspan="7"><b>BibTeX</b>:
     824<pre>
     825@article{mcmillan00methodology,
     826  author = {K.L. McMillan},
     827  title = {A Methodology for Hardware Verification Using Compositional Model Checking},
     828  journal = {Science of Computer Programming},
     829  year = {2000},
     830  volume = {37},
     831  number = {1--3},
     832  pages = {279--309},
     833  url = {citeseer.ist.psu.edu/mcmillan99methodology.html}
     834}
     835</pre></td>
     836</tr>
     837<tr id="DBLP:conf/cav/McMillan97" class="entry">
     838        <td>McMillan, K.L.&nbsp;Orna Grumberg (Ed.)</td>
     839        <td>A Compositional Rule for Hardware Design Refinement. <p class="infolinks">[<a href="javascript:toggleInfo('DBLP:conf/cav/McMillan97','bibtex')">BibTeX</a>]</p></td>
     840        <td>1997</td>
     841        <td><br/>Vol. 1254CAV'97: Proceedings of the 9th International Conference on Computer Aided Verification, pp. 24-35&nbsp;</td>
     842        <td>inproceedings</td>
     843        <td>&nbsp;</td>
     844</tr>
     845<tr id="bib_DBLP:conf/cav/McMillan97" class="bibtex noshow">
     846<td colspan="7"><b>BibTeX</b>:
     847<pre>
     848@inproceedings{DBLP:conf/cav/McMillan97,
     849  author = {Kenneth L. McMillan},
     850  title = {A Compositional Rule for Hardware Design Refinement.},
     851  booktitle = {CAV'97: Proceedings of the 9th International Conference on Computer Aided Verification},
     852  publisher = {Springer},
     853  year = {1997},
     854  volume = {1254},
     855  pages = {24-35}
     856}
     857</pre></td>
     858</tr>
     859<tr id="peng02thesis" class="entry">
     860        <td>Peng, H.&nbsp;</td>
     861        <td>Improving Compositional Verification through Environment Synthesis and Syntactic Model Reduction <p class="infolinks">[<a href="javascript:toggleInfo('peng02thesis','bibtex')">BibTeX</a>]</p></td>
     862        <td>2002</td>
     863        <td><i>School</i>: Dept. of Electrical and Computer Engenering, Concordia University, Montreal, Quebec, Canada&nbsp;</td>
     864        <td>phdthesis</td>
     865        <td>&nbsp;</td>
     866</tr>
     867<tr id="bib_peng02thesis" class="bibtex noshow">
     868<td colspan="7"><b>BibTeX</b>:
     869<pre>
     870@phdthesis{peng02thesis,
     871  author = {H.~Peng},
     872  title = {Improving Compositional Verification through Environment Synthesis and Syntactic Model Reduction},
     873  school = {Dept. of Electrical and Computer Engenering, Concordia University, Montreal, Quebec, Canada},
     874  year = {2002}
     875}
     876</pre></td>
     877</tr>
     878<tr id="peng02tableau" class="entry">
     879        <td>Peng, H., Mokhtari, Y. &amp; Tahar, S.&nbsp;</td>
     880        <td>Environment Synthesis for Compositional Model Checking. <p class="infolinks">[<a href="javascript:toggleInfo('peng02tableau','bibtex')">BibTeX</a>]</p></td>
     881        <td>2002</td>
     882        <td>ICCD'02: Proceedings of the 20th International Conference on Computer Design, pp. 70-&nbsp;</td>
     883        <td>inproceedings</td>
     884        <td>&nbsp;</td>
     885</tr>
     886<tr id="bib_peng02tableau" class="bibtex noshow">
     887<td colspan="7"><b>BibTeX</b>:
     888<pre>
     889@inproceedings{peng02tableau,
     890  author = {H.~Peng and Y.~Mokhtari and S.~Tahar},
     891  title = {Environment Synthesis for Compositional Model Checking.},
     892  booktitle = {ICCD'02: Proceedings of the 20th International Conference on Computer Design},
     893  publisher = {IEEE Computer Society},
     894  year = {2002},
     895  pages = {70-}
     896}
     897</pre></td>
     898</tr>
    619899<tr id="Tripakis201" class="entry">
    620900        <td>Tripakis, S., Andrade, H., Ghosal, A., Limaye, R., Ravindran, K., Wang, G., Yang, G., Kormerup, J. &amp; Wong, I.&nbsp;</td>
    … …  
    643923</pre></td>
    644924</tr>
    645 
    646 <tr id="6128043" class="entry">
    647         <td>Feng, Y., Veeramani, A., Kanagasabai, R. &amp; Rho, S.&nbsp;</td>
    648         <td>Automatic Service Composition via Model Checking <p class="infolinks">[<a href="javascript:toggleInfo('6128043','abstract')">Abstract</a>] [<a href="javascript:toggleInfo('6128043','bibtex')">BibTeX</a>]</p></td>
    649         <td>2011</td>
    650         <td>Services Computing Conference (APSCC), 2011 IEEE Asia-Pacific, pp. 477 -482&nbsp;</td>
    651         <td>inproceedings</td>
    652         <td><a href="http://dx.doi.org/10.1109/APSCC.2011.54">DOI</a> &nbsp;</td>
    653 </tr>
    654 <tr id="abs_6128043" class="abstract noshow">
    655         <td colspan="7"><b>Abstract</b>: 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.</td>
    656 </tr>
    657 <tr id="bib_6128043" class="bibtex noshow">
    658 <td colspan="7"><b>BibTeX</b>:
    659 <pre>
    660 @inproceedings{6128043,
    661   author = {Yuzhang Feng and Veeramani, A. and Kanagasabai, R. and Seungmin Rho},
    662   title = {Automatic Service Composition via Model Checking},
    663   booktitle = {Services Computing Conference (APSCC), 2011 IEEE Asia-Pacific},
    664   year = {2011},
    665   pages = {477 -482},
    666   doi = {http://dx.doi.org/10.1109/APSCC.2011.54}
     925<tr id="xie03verified" class="entry">
     926        <td>Xie, F. &amp; Browne, J.&nbsp;</td>
     927        <td>Verified Systems by Composition from Verified Components <p class="infolinks">[<a href="javascript:toggleInfo('xie03verified','bibtex')">BibTeX</a>]</p></td>
     928        <td>2003</td>
     929        <td>ESEC/FSE 2003 : Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering 2003 held jointly with 9th European Software Engineering Conference, pp. 277-286&nbsp;</td>
     930        <td>inproceedings</td>
     931        <td><a href="http://doi.acm.org/10.1145/940071.940109">DOI</a> &nbsp;</td>
     932</tr>
     933<tr id="bib_xie03verified" class="bibtex noshow">
     934<td colspan="7"><b>BibTeX</b>:
     935<pre>
     936@inproceedings{xie03verified,
     937  author = {F.~Xie and J.C.~Browne},
     938  title = {Verified Systems by Composition from Verified Components},
     939  booktitle = {ESEC/FSE 2003 : Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering 2003 held jointly with 9th European Software Engineering Conference},
     940  publisher = {ACM Press},
     941  year = {2003},
     942  pages = {277--286},
     943  doi = {http://doi.acm.org/10.1145/940071.940109}
    667944}
    668945</pre></td>
    … …  
    680957</tr>
    681958<tr id="rev_5374376" class="review noshow">
    682         <td colspan="7"><b>Review</b>: 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 :
    683 <ul>
    684 <li>     to identify and remove unsynchronized behavior.
    685  <li> to extend the refinement to more than two components itemize
    686 </ul>
    687 
    688 Main contribution : Local synchronization detection method for component based on parallel composition and an AR methof for modular MC.
    689 <br>
    690 Circuit class : Asynchronous</td>
    691 
    692 </tr>
    693 
     959        <td colspan="7"><b>Review</b>: 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 : <p><ul><p><li>     to identify and remove unsynchronized behavior. <p> <li> to extend the refinement to more than two components itemize <p></ul><p>Main contribution : Local synchronization detection method for component based on parallel composition and an AR methof for modular MC.<p><br><p>Circuit class : Asynchronous</td></td>
     960</tr>
    694961<tr id="bib_5374376" class="bibtex noshow">
    695962<td colspan="7"><b>BibTeX</b>:
    … …  
    707974</pre></td>
    708975</tr>
    709 
    710 
    711 
    712976</tbody>
    713977</table>
    714978
    715 
    716979<p>
    717  <small>Created by <a href="http://jabref.sourceforge.net">JabRef</a> on 28/02/2012.</small>
     980 <small>Created by <a href="http://jabref.sourceforge.net">JabRef</a> on 07/03/2012.</small>
    718981</p>
    719 
    720982
    721983</body>
    … …  
    723985
    724986<!-- File generated by JabRef ; Export Filter written by Mark Schenk -->
    725 
    726987}}}