1 | <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd"> |
---|
2 | <html lang="en"> |
---|
3 | <head> |
---|
4 | <title>JabRef References output</title> |
---|
5 | <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"> |
---|
6 | <script type="text/javascript"> |
---|
7 | <!-- |
---|
8 | // QuickSearch script for JabRef HTML export |
---|
9 | // Version: 2.0 |
---|
10 | // |
---|
11 | // Copyright (c) 2006-2008, Mark Schenk |
---|
12 | // |
---|
13 | // This software is distributed under a Creative Commons Attribution 3.0 License |
---|
14 | // http://creativecommons.org/licenses/by/3.0/ |
---|
15 | |
---|
16 | // Some features: |
---|
17 | // + optionally searches Abstracts and Reviews |
---|
18 | // + allows RegExp searches |
---|
19 | // e.g. to search for entries between 1980 and 1989, type: 198[0-9] |
---|
20 | // e.g. for any entry ending with 'symmetry', type: symmetry$ |
---|
21 | // e.g. for all reftypes that are books: ^book$, or ^article$ |
---|
22 | // e.g. for entries by either John or Doe, type john|doe |
---|
23 | // + easy toggling of Abstract/Review/BibTeX |
---|
24 | |
---|
25 | // Search settings |
---|
26 | var searchAbstract = true; |
---|
27 | var searchReview = true; |
---|
28 | |
---|
29 | // Speed optimisation introduced some esoteric problems with certain RegExp searches |
---|
30 | // e.g. if the previous search is 200[-7] and the next search is 200[4-7] then the search doesn't work properly until the next 'keyup' |
---|
31 | // hence the searchOpt can be turned off for RegExp adepts |
---|
32 | var searchOpt = true; |
---|
33 | |
---|
34 | if (window.addEventListener) { |
---|
35 | window.addEventListener("load",initSearch,false); } |
---|
36 | else if (window.attachEvent) { |
---|
37 | window.attachEvent("onload", initSearch); } |
---|
38 | |
---|
39 | function initSearch() { |
---|
40 | // basic object detection |
---|
41 | if(!document.getElementById || !document.getElementsByTagName) { return; } |
---|
42 | if (!document.getElementById('qstable')||!document.getElementById('qs')) { return; } |
---|
43 | |
---|
44 | // find QS table and appropriate rows |
---|
45 | searchTable = document.getElementById('qstable'); |
---|
46 | var allRows = searchTable.getElementsByTagName('tbody')[0].getElementsByTagName('tr'); |
---|
47 | |
---|
48 | // split all rows into entryRows and infoRows (e.g. abstract, review, bibtex) |
---|
49 | entryRows = new Array(); |
---|
50 | infoRows = new Array(); absRows = new Array(); revRows = new Array(); |
---|
51 | |
---|
52 | for (var i=0, k=0, j=0; i<allRows.length;i++) { |
---|
53 | if (allRows[i].className.match(/entry/)) { |
---|
54 | entryRows[j++] = allRows[i]; |
---|
55 | } else { |
---|
56 | infoRows[k++] = allRows[i]; |
---|
57 | // check for abstract/review |
---|
58 | if (allRows[i].className.match(/abstract/)) { |
---|
59 | absRows.push(allRows[i]); |
---|
60 | } else if (allRows[i].className.match(/review/)) { |
---|
61 | revRows.push(allRows[i]); |
---|
62 | } |
---|
63 | } |
---|
64 | } |
---|
65 | |
---|
66 | //number of entries and rows |
---|
67 | numRows = allRows.length; |
---|
68 | numEntries = entryRows.length; |
---|
69 | numInfo = infoRows.length; |
---|
70 | numAbs = absRows.length; |
---|
71 | numRev = revRows.length; |
---|
72 | |
---|
73 | //find the query field |
---|
74 | qsfield = document.getElementById('qsfield'); |
---|
75 | |
---|
76 | // previous search term; used for speed optimisation |
---|
77 | prevSearch = ''; |
---|
78 | |
---|
79 | //find statistics location |
---|
80 | stats = document.getElementById('stat'); |
---|
81 | setStatistics(-1); |
---|
82 | |
---|
83 | // creates the appropriate search settings |
---|
84 | createQSettingsDialog(); |
---|
85 | |
---|
86 | // shows the searchfield |
---|
87 | document.getElementById('qs').style.display = 'block'; |
---|
88 | document.getElementById('qsfield').onkeyup = testEvent; |
---|
89 | } |
---|
90 | |
---|
91 | function quickSearch(tInput){ |
---|
92 | |
---|
93 | if (tInput.value.length == 0) { |
---|
94 | showAll(); |
---|
95 | setStatistics(-1); |
---|
96 | qsfield.className = ''; |
---|
97 | return; |
---|
98 | } else { |
---|
99 | // only search for valid RegExp |
---|
100 | try { |
---|
101 | var searchText = new RegExp(tInput.value,"i") |
---|
102 | closeAllInfo(); |
---|
103 | qsfield.className = ''; |
---|
104 | } |
---|
105 | catch(err) { |
---|
106 | prevSearch = tInput.value; |
---|
107 | qsfield.className = 'invalidsearch'; |
---|
108 | return; |
---|
109 | } |
---|
110 | } |
---|
111 | |
---|
112 | // count number of hits |
---|
113 | var hits = 0; |
---|
114 | |
---|
115 | // start looping through all entry rows |
---|
116 | for (var i = 0; cRow = entryRows[i]; i++){ |
---|
117 | |
---|
118 | // only show search the cells if it isn't already hidden OR if the search term is getting shorter, then search all |
---|
119 | // some further optimisation is possible: if the search string is getting shorter, and the row is already visible, skip it. Then be careful with hits! |
---|
120 | if(!searchOpt || cRow.className.indexOf('noshow')==-1 || tInput.value.length <= prevSearch.length){ |
---|
121 | var found = false; |
---|
122 | |
---|
123 | var inCells = cRow.getElementsByTagName('td'); |
---|
124 | var numCols = inCells.length; |
---|
125 | |
---|
126 | for (var j=0; j<numCols; j++) { |
---|
127 | cCell = inCells[j]; |
---|
128 | var t = cCell.innerText?cCell.innerText:getTextContent(cCell); |
---|
129 | if (t.search(searchText) != -1){ |
---|
130 | found=true; |
---|
131 | break; |
---|
132 | } |
---|
133 | } |
---|
134 | |
---|
135 | // look for further hits in Abstract and Review |
---|
136 | if(!found) { |
---|
137 | var articleid = cRow.id; |
---|
138 | if(searchAbstract && (abs = document.getElementById('abs_'+articleid))) { |
---|
139 | if (getTextContent(abs).search(searchText) != -1){ found=true; } |
---|
140 | } |
---|
141 | if(searchReview && (rev = document.getElementById('rev_'+articleid))) { |
---|
142 | if (getTextContent(rev).search(searchText) != -1){ found=true; } |
---|
143 | } |
---|
144 | } |
---|
145 | |
---|
146 | if(found) { |
---|
147 | cRow.className = 'entry show'; |
---|
148 | hits++; |
---|
149 | } else { |
---|
150 | cRow.className = 'entry noshow'; |
---|
151 | } |
---|
152 | } |
---|
153 | } |
---|
154 | |
---|
155 | // update statistics |
---|
156 | setStatistics(hits) |
---|
157 | |
---|
158 | // set previous search value |
---|
159 | prevSearch = tInput.value; |
---|
160 | } |
---|
161 | |
---|
162 | function toggleInfo(articleid,info) { |
---|
163 | |
---|
164 | var entry = document.getElementById(articleid); |
---|
165 | var abs = document.getElementById('abs_'+articleid); |
---|
166 | var rev = document.getElementById('rev_'+articleid); |
---|
167 | var bib = document.getElementById('bib_'+articleid); |
---|
168 | // Get the abstracts/reviews/bibtext in the right location |
---|
169 | // in unsorted tables this is always the case, but in sorted tables it is necessary. |
---|
170 | // Start moving in reverse order, so we get: entry, abstract,review,bibtex |
---|
171 | if (searchTable.className.indexOf('sortable') != -1) { |
---|
172 | if(bib) { entry.parentNode.insertBefore(bib,entry.nextSibling); } |
---|
173 | if(rev) { entry.parentNode.insertBefore(rev,entry.nextSibling); } |
---|
174 | if(abs) { entry.parentNode.insertBefore(abs,entry.nextSibling); } |
---|
175 | } |
---|
176 | |
---|
177 | if (abs && info == 'abstract') { |
---|
178 | if(abs.className.indexOf('abstract') != -1) { |
---|
179 | abs.className.indexOf('noshow') == -1?abs.className = 'abstract noshow':abs.className = 'abstract'; |
---|
180 | } |
---|
181 | } else if (rev && info == 'review') { |
---|
182 | if(rev.className.indexOf('review') != -1) { |
---|
183 | rev.className.indexOf('noshow') == -1?rev.className = 'review noshow':rev.className = 'review'; |
---|
184 | } |
---|
185 | } else if (bib && info == 'bibtex') { |
---|
186 | if(bib.className.indexOf('bibtex') != -1) { |
---|
187 | bib.className.indexOf('noshow') == -1?bib.className = 'bibtex noshow':bib.className = 'bibtex'; |
---|
188 | } |
---|
189 | } else { |
---|
190 | return; |
---|
191 | } |
---|
192 | |
---|
193 | // check if one or the other is available |
---|
194 | var revshow = false; |
---|
195 | var absshow = false; |
---|
196 | var bibshow = false; |
---|
197 | (abs && abs.className.indexOf('noshow') == -1)? absshow = true: absshow = false; |
---|
198 | (rev && rev.className.indexOf('noshow') == -1)? revshow = true: revshow = false; |
---|
199 | (bib && bib.className == 'bibtex')? bibshow = true: bibshow = false; |
---|
200 | |
---|
201 | // highlight original entry |
---|
202 | if(entry) { |
---|
203 | if (revshow || absshow || bibshow) { |
---|
204 | entry.className = 'entry highlight show'; |
---|
205 | } else { |
---|
206 | entry.className = 'entry show'; |
---|
207 | } |
---|
208 | } |
---|
209 | |
---|
210 | // When there's a combination of abstract/review/bibtex showing, need to add class for correct styling |
---|
211 | if(absshow) { |
---|
212 | (revshow||bibshow)?abs.className = 'abstract nextshow':abs.className = 'abstract'; |
---|
213 | } |
---|
214 | if (revshow) { |
---|
215 | bibshow?rev.className = 'review nextshow': rev.className = 'review'; |
---|
216 | } |
---|
217 | |
---|
218 | } |
---|
219 | |
---|
220 | function setStatistics (hits) { |
---|
221 | if(hits < 0) { hits=numEntries; } |
---|
222 | if(stats) { stats.firstChild.data = hits + '/' + numEntries} |
---|
223 | } |
---|
224 | |
---|
225 | function getTextContent(node) { |
---|
226 | // Function written by Arve Bersvendsen |
---|
227 | // http://www.virtuelvis.com |
---|
228 | |
---|
229 | if (node.nodeType == 3) { |
---|
230 | return node.nodeValue; |
---|
231 | } // text node |
---|
232 | if (node.nodeType == 1) { // element node |
---|
233 | var text = []; |
---|
234 | for (var chld = node.firstChild;chld;chld=chld.nextSibling) { |
---|
235 | text.push(getTextContent(chld)); |
---|
236 | } |
---|
237 | return text.join(""); |
---|
238 | } return ""; // some other node, won't contain text nodes. |
---|
239 | } |
---|
240 | |
---|
241 | function showAll(){ |
---|
242 | // first close all abstracts, reviews, etc. |
---|
243 | closeAllInfo(); |
---|
244 | |
---|
245 | for (var i = 0; i < numEntries; i++){ |
---|
246 | entryRows[i].className = 'entry show'; |
---|
247 | } |
---|
248 | } |
---|
249 | |
---|
250 | function closeAllInfo(){ |
---|
251 | for (var i=0; i < numInfo; i++){ |
---|
252 | if (infoRows[i].className.indexOf('noshow') ==-1) { |
---|
253 | infoRows[i].className = infoRows[i].className + ' noshow'; |
---|
254 | } |
---|
255 | } |
---|
256 | } |
---|
257 | |
---|
258 | function testEvent(e){ |
---|
259 | if (!e) var e = window.event; |
---|
260 | quickSearch(this); |
---|
261 | } |
---|
262 | |
---|
263 | function clearQS() { |
---|
264 | qsfield.value = ''; |
---|
265 | quickSearch(qsfield); |
---|
266 | } |
---|
267 | |
---|
268 | function redoQS(){ |
---|
269 | showAll(); |
---|
270 | quickSearch(qsfield); |
---|
271 | } |
---|
272 | |
---|
273 | // Create Search Settings |
---|
274 | |
---|
275 | function toggleQSettingsDialog() { |
---|
276 | |
---|
277 | var qssettings = document.getElementById('qssettings'); |
---|
278 | |
---|
279 | if(qssettings.className.indexOf('active')==-1) { |
---|
280 | qssettings.className = 'active'; |
---|
281 | |
---|
282 | if(absCheckBox && searchAbstract == true) { absCheckBox.checked = 'checked'; } |
---|
283 | if(revCheckBox && searchReview == true) { revCheckBox.checked = 'checked'; } |
---|
284 | |
---|
285 | } else { |
---|
286 | qssettings.className= ''; |
---|
287 | } |
---|
288 | } |
---|
289 | |
---|
290 | function createQSettingsDialog(){ |
---|
291 | var qssettingslist = document.getElementById('qssettings').getElementsByTagName('ul')[0]; |
---|
292 | |
---|
293 | if(numAbs!=0) { |
---|
294 | var x = document.createElement('input'); |
---|
295 | x.id = "searchAbs"; |
---|
296 | x.type = "checkbox"; |
---|
297 | x.onclick = toggleQSetting; |
---|
298 | var y = qssettingslist.appendChild(document.createElement('li')).appendChild(document.createElement('label')); |
---|
299 | y.appendChild(x); |
---|
300 | y.appendChild(document.createTextNode('search abstracts')); |
---|
301 | } |
---|
302 | if(numRev!=0) { |
---|
303 | var x = document.createElement('input'); |
---|
304 | x.id = "searchRev"; |
---|
305 | x.type = "checkbox"; |
---|
306 | x.onclick = toggleQSetting; |
---|
307 | var y = qssettingslist.appendChild(document.createElement('li')).appendChild(document.createElement('label')); |
---|
308 | y.appendChild(x); |
---|
309 | y.appendChild(document.createTextNode('search reviews')); |
---|
310 | } |
---|
311 | |
---|
312 | // global variables |
---|
313 | absCheckBox = document.getElementById('searchAbs'); |
---|
314 | revCheckBox = document.getElementById('searchRev'); |
---|
315 | |
---|
316 | // show search settings |
---|
317 | if(absCheckBox||revCheckBox) { |
---|
318 | document.getElementById('qssettings').style.display = 'block'; |
---|
319 | } |
---|
320 | } |
---|
321 | |
---|
322 | function toggleQSetting() { |
---|
323 | if(this.id=='searchAbs') { searchAbstract = !searchAbstract; } |
---|
324 | if(this.id=='searchRev') { searchReview = !searchReview; } |
---|
325 | redoQS() |
---|
326 | } |
---|
327 | --> |
---|
328 | </script> |
---|
329 | <script type="text/javascript"> |
---|
330 | <!-- |
---|
331 | // Sort Table Script |
---|
332 | // Version: 1.1 |
---|
333 | // |
---|
334 | // Copyright (c) 2006-2008, Mark Schenk |
---|
335 | // |
---|
336 | // This software is distributed under a Creative Commons Attribution 3.0 License |
---|
337 | // http://creativecommons.org/licenses/by/3.0/ |
---|
338 | |
---|
339 | // NB: slow as molasses in FireFox, especially when sorting columns with a lot of text. |
---|
340 | // An optimization is implemented which makes speed bearable, toggled by the following variable |
---|
341 | var SORT_SPEED_OPT = true; |
---|
342 | // a bit of browser preference: Opera does not need optimization |
---|
343 | if(window.opera) { SORT_SPEED_OPT=false; } |
---|
344 | // the optimization has one limitation on the functionality: when sorting search |
---|
345 | // results, the expanded info, e.g. bibtex/review, is collapsed. In the non-optimized |
---|
346 | // version they remain visible. |
---|
347 | |
---|
348 | |
---|
349 | if (window.addEventListener) { |
---|
350 | window.addEventListener("load",initSortTable,false) } |
---|
351 | else if (window.attachEvent) { |
---|
352 | window.attachEvent("onload", initSortTable); } |
---|
353 | |
---|
354 | function initSortTable() { |
---|
355 | var alltables = document.getElementsByTagName('table'); |
---|
356 | for(i=0;i<alltables.length;i++) { |
---|
357 | var currentTable = alltables[i]; |
---|
358 | if(currentTable.className.indexOf('sortable') !=-1) { |
---|
359 | var thead = currentTable.getElementsByTagName('thead')[0]; |
---|
360 | thead.title = 'Click on any column header to sort'; |
---|
361 | for (var i=0;cell = thead.getElementsByTagName('th')[i];i++) { |
---|
362 | cell.onclick = function () { resortTable(this); }; |
---|
363 | // make it possible to have a default sort column |
---|
364 | if(cell.className.indexOf('sort')!=-1) { |
---|
365 | resortTable(cell) |
---|
366 | } |
---|
367 | } |
---|
368 | } |
---|
369 | } |
---|
370 | } |
---|
371 | |
---|
372 | var SORT_COLUMN_INDEX |
---|
373 | |
---|
374 | function resortTable(td) { |
---|
375 | var column = td.cellIndex; |
---|
376 | var table = getParent(td,'TABLE'); |
---|
377 | |
---|
378 | var allRows = table.getElementsByTagName('tbody')[0].getElementsByTagName('tr'); |
---|
379 | var newRows = new Array(); |
---|
380 | |
---|
381 | for (var i=0, k=0; i<allRows.length;i++) { |
---|
382 | |
---|
383 | var rowclass = allRows[i].className; |
---|
384 | |
---|
385 | if (rowclass.indexOf('entry') != -1) { |
---|
386 | newRows[k++] = allRows[i]; |
---|
387 | } |
---|
388 | |
---|
389 | if (SORT_SPEED_OPT) { |
---|
390 | // remove highlight class |
---|
391 | allRows[i].className = rowclass.replace(/highlight/,''); |
---|
392 | // close information |
---|
393 | if(rowclass.indexOf('entry') == -1 && rowclass.indexOf('noshow') == -1) { allRows[i].className = rowclass + ' noshow';} |
---|
394 | } |
---|
395 | } |
---|
396 | |
---|
397 | |
---|
398 | // If other sort functions are deemed necessary (e.g. for |
---|
399 | // dates and currencies) they can be added. |
---|
400 | var sortfn = ts_sort_firstchild_caseinsensitive; |
---|
401 | SORT_COLUMN_INDEX = column; |
---|
402 | newRows.sort(sortfn); |
---|
403 | |
---|
404 | // create a container for showing sort arrow |
---|
405 | var arrow = td.getElementsByTagName('span')[0]; |
---|
406 | if (!arrow) { var arrow = td.appendChild(document.createElement('span'));} |
---|
407 | |
---|
408 | if (td.className) { |
---|
409 | if (td.className.indexOf('sort_asc') !=-1) { |
---|
410 | td.className = td.className.replace(/_asc/,"_des"); |
---|
411 | newRows.reverse(); |
---|
412 | arrow.innerHTML = '⇑'; |
---|
413 | } else if (td.className.indexOf('sort_des') !=-1) { |
---|
414 | td.className = td.className.replace(/_des/,"_asc"); |
---|
415 | arrow.innerHTML = '⇓'; |
---|
416 | } else { |
---|
417 | td.className += ' sort_asc'; |
---|
418 | arrow.innerHTML = '⇓'; |
---|
419 | } |
---|
420 | } else { |
---|
421 | td.className += 'sort_asc'; |
---|
422 | arrow.innerHTML = '⇓'; |
---|
423 | } |
---|
424 | |
---|
425 | // Remove the classnames and up/down arrows for the other headers |
---|
426 | var ths = table.getElementsByTagName('thead')[0].getElementsByTagName('th'); |
---|
427 | for (var i=0; i<ths.length; i++) { |
---|
428 | if(ths[i]!=td && ths[i].className.indexOf('sort_')!=-1) { |
---|
429 | // argh, moronic JabRef thinks (backslash)w is an output field!! |
---|
430 | //ths[i].className = ths[i].className.replace(/sort_(backslash)w{3}/,""); |
---|
431 | ths[i].className = ths[i].className.replace(/sort_asc/,""); |
---|
432 | ths[i].className = ths[i].className.replace(/sort_des/,""); |
---|
433 | |
---|
434 | // remove span |
---|
435 | var arrow = ths[i].getElementsByTagName('span')[0]; |
---|
436 | if (arrow) { ths[i].removeChild(arrow); } |
---|
437 | } |
---|
438 | } |
---|
439 | |
---|
440 | // We appendChild rows that already exist to the tbody, so it moves them rather than creating new ones |
---|
441 | for (i=0;i<newRows.length;i++) { |
---|
442 | table.getElementsByTagName('tbody')[0].appendChild(newRows[i]); |
---|
443 | |
---|
444 | if(!SORT_SPEED_OPT){ |
---|
445 | // moving additional information, e.g. bibtex/abstract to right locations |
---|
446 | // this allows to sort, even with abstract/review/etc. still open |
---|
447 | var articleid = newRows[i].id; |
---|
448 | |
---|
449 | var entry = document.getElementById(articleid); |
---|
450 | var abs = document.getElementById('abs_'+articleid); |
---|
451 | var rev = document.getElementById('rev_'+articleid); |
---|
452 | var bib = document.getElementById('bib_'+articleid); |
---|
453 | |
---|
454 | var tbody = table.getElementsByTagName('tbody')[0]; |
---|
455 | // mind the order of adding the entries |
---|
456 | if(abs) { tbody.appendChild(abs); } |
---|
457 | if(rev) { tbody.appendChild(rev); } |
---|
458 | if(bib) { tbody.appendChild(bib); } |
---|
459 | } |
---|
460 | } |
---|
461 | } |
---|
462 | |
---|
463 | function ts_sort_firstchild_caseinsensitive(a,b) { |
---|
464 | // only search in .firstChild of the cells. Speeds things up tremendously in FF |
---|
465 | // problem is that it won't find all the text in a cell if the firstChild is an element |
---|
466 | // or if there are other elements in the cell. Risky fix, but the speed boost is worth it. |
---|
467 | var acell = a.cells[SORT_COLUMN_INDEX]; |
---|
468 | var bcell = b.cells[SORT_COLUMN_INDEX]; |
---|
469 | |
---|
470 | acell.firstChild? aa = getTextContent(acell.firstChild).toLowerCase():aa = ""; |
---|
471 | bcell.firstChild? bb = getTextContent(bcell.firstChild).toLowerCase():bb = ""; |
---|
472 | |
---|
473 | if (aa==bb) return 0; |
---|
474 | if (aa<bb) return -1; |
---|
475 | return 1; |
---|
476 | } |
---|
477 | |
---|
478 | function ts_sort_caseinsensitive(a,b) { |
---|
479 | aa = getTextContent(a.cells[SORT_COLUMN_INDEX]).toLowerCase(); |
---|
480 | bb = getTextContent(b.cells[SORT_COLUMN_INDEX]).toLowerCase(); |
---|
481 | if (aa==bb) return 0; |
---|
482 | if (aa<bb) return -1; |
---|
483 | return 1; |
---|
484 | } |
---|
485 | |
---|
486 | function ts_sort_default(a,b) { |
---|
487 | aa = getTextContent(a.cells[SORT_COLUMN_INDEX]); |
---|
488 | bb = getTextContent(b.cells[SORT_COLUMN_INDEX]); |
---|
489 | if (aa==bb) return 0; |
---|
490 | if (aa<bb) return -1; |
---|
491 | return 1; |
---|
492 | } |
---|
493 | |
---|
494 | function getParent(el, pTagName) { |
---|
495 | if (el == null) { |
---|
496 | return null; |
---|
497 | } else if (el.nodeType == 1 && el.tagName.toLowerCase() == pTagName.toLowerCase()) { |
---|
498 | return el; |
---|
499 | } else { |
---|
500 | return getParent(el.parentNode, pTagName); |
---|
501 | } |
---|
502 | } |
---|
503 | --> |
---|
504 | </script> |
---|
505 | |
---|
506 | <style type="text/css"> |
---|
507 | body { background-color: white; font-family: "Trebuchet MS", Arial, sans-serif; font-size: 12px; line-height: 1.2; padding: 1em; color: #2E2E2E; } |
---|
508 | |
---|
509 | #qs { width: auto; border-style: solid; border-color: gray; border-width: 1px 1px 0px 1px; padding: 0.5em 0.5em; display:none; position:relative; } |
---|
510 | #qs form { padding: 0px; margin: 0px; } |
---|
511 | #qs form p { padding: 0px; margin: 0px; } |
---|
512 | |
---|
513 | .invalidsearch { background-color: red; } |
---|
514 | |
---|
515 | table { border: 1px gray solid; width: 100%; empty-cells: show; } |
---|
516 | th, td { border: 1px gray solid; padding: 0.5em; vertical-align: top; } |
---|
517 | td { text-align: left; vertical-align: top; } |
---|
518 | th { background-color: #EFEFEF; } |
---|
519 | |
---|
520 | td a { color: navy; text-decoration: none; } |
---|
521 | td a:hover { text-decoration: underline; } |
---|
522 | |
---|
523 | tr.noshow { display: none;} |
---|
524 | |
---|
525 | tr.highlight td { background-color: #F1F1F1; border-top: 2px black solid; font-weight: bold; } |
---|
526 | tr.abstract td, tr.review td, tr.bibtex td { background-color: #F1F1F1; border-bottom: 2px black solid; } |
---|
527 | tr.nextshow td { border-bottom: 1px gray solid; } |
---|
528 | |
---|
529 | tr.bibtex pre { width: 100%; overflow: auto;} |
---|
530 | |
---|
531 | p.infolinks { margin: 0.5em 0em 0em 0em; padding: 0px; } |
---|
532 | |
---|
533 | #qssettings { padding: 0.5em; position: absolute; top: 0.2em; right: 0.2em; border: 1px gray solid; background-color: white; display: none; } |
---|
534 | #qssettings p { font-weight: bold; cursor: pointer; } |
---|
535 | #qssettings ul { display: none; list-style-type: none; padding-left: 0; margin: 0; } |
---|
536 | #qssettings.active ul { display: block; } |
---|
537 | |
---|
538 | @media print { |
---|
539 | p.infolinks, #qssettings, #qs { display: none !important; } |
---|
540 | table { border-width: 0px; } |
---|
541 | tr { page-break-inside: avoid; } |
---|
542 | tr > * + * + * + * + * {display: none; } |
---|
543 | thead tr::before { content: "Reference"; border: 1px gray solid; padding: 0.5em; vertical-align: top; font-weight: bold; text-align: center; display: table-cell; background-color: #EFEFEF; } |
---|
544 | tr[id]::before { content: attr(id); display: table-cell; border: 1px gray solid; padding: 0.5em; vertical-align: top; font-style: italic; } |
---|
545 | } |
---|
546 | th.sort_asc, th.sort_des { border: 2px black solid; } |
---|
547 | |
---|
548 | </style> |
---|
549 | </head> |
---|
550 | <body> |
---|
551 | |
---|
552 | <div id="qs"> |
---|
553 | <form action=""> |
---|
554 | <p>QuickSearch: <input type="text" name="qsfield" id="qsfield" autocomplete="off" title="Allows plain text as well as RegExp searches" /><input type="button" onclick="clearQS()" value="clear" /> Number of matching entries: <span id="stat">0</span>.</p> |
---|
555 | <div id="qssettings"> |
---|
556 | <p onclick="toggleQSettingsDialog()">Search Settings</p> |
---|
557 | <ul></ul> |
---|
558 | </div> |
---|
559 | </form> |
---|
560 | </div> |
---|
561 | <table id="qstable" class="sortable" border="1"> |
---|
562 | <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> |
---|
563 | <tbody> |
---|
564 | <tr id="alder06ticc" class="entry"> |
---|
565 | <td>Adler, B., de Alfaro, L., da Silva, L.D., Faella, M., Legay, A., Raman, V. & Roy, P. Thomas Ball and Robert B. Jones (Ed.)</td> |
---|
566 | <td>Ticc: A Tool for Interface Compatibility and Composition. <p class="infolinks">[<a href="javascript:toggleInfo('alder06ticc','bibtex')">BibTeX</a>]</p></td> |
---|
567 | <td>2006</td> |
---|
568 | <td><br/>Vol. 4144CAV'06: Proceedings of 18th International Conference of Computer Aided Verification, pp. 59-62 </td> |
---|
569 | <td>inproceedings</td> |
---|
570 | <td> </td> |
---|
571 | </tr> |
---|
572 | <tr id="bib_alder06ticc" class="bibtex noshow"> |
---|
573 | <td colspan="7"><b>BibTeX</b>: |
---|
574 | <pre> |
---|
575 | @inproceedings{alder06ticc, |
---|
576 | 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}, |
---|
577 | title = {Ticc: A Tool for Interface Compatibility and Composition.}, |
---|
578 | booktitle = {CAV'06: Proceedings of 18th International Conference of Computer Aided Verification}, |
---|
579 | year = {2006}, |
---|
580 | volume = {4144}, |
---|
581 | pages = {59-62} |
---|
582 | } |
---|
583 | </pre></td> |
---|
584 | </tr> |
---|
585 | <tr id="amla01assume" class="entry"> |
---|
586 | <td>Amla, N., Emerson, E.A., Namjoshi, K.S. & Trefler, R.J. </td> |
---|
587 | <td>Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams <p class="infolinks">[<a href="javascript:toggleInfo('amla01assume','bibtex')">BibTeX</a>]</p></td> |
---|
588 | <td>2001</td> |
---|
589 | <td>TACAS 2001: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 465-479 </td> |
---|
590 | <td>inproceedings</td> |
---|
591 | <td> </td> |
---|
592 | </tr> |
---|
593 | <tr id="bib_amla01assume" class="bibtex noshow"> |
---|
594 | <td colspan="7"><b>BibTeX</b>: |
---|
595 | <pre> |
---|
596 | @inproceedings{amla01assume, |
---|
597 | author = {N.~Amla and E.~A.~Emerson and K.~S.~Namjoshi and R.~J.~Trefler}, |
---|
598 | title = {Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams}, |
---|
599 | booktitle = {TACAS 2001: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, |
---|
600 | publisher = {Springer-Verlag}, |
---|
601 | year = {2001}, |
---|
602 | pages = {465--479} |
---|
603 | } |
---|
604 | </pre></td> |
---|
605 | </tr> |
---|
606 | <tr id="Cabodi09Speeding" class="entry"> |
---|
607 | <td>Cabodi, G., Camurati, P., Garcia, L., Murciano, M., Nocco, S. & Quer, S. </td> |
---|
608 | <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> |
---|
609 | <td>2009</td> |
---|
610 | <td>DATE '09: Proceedings of the conference on Design, Automation and Test in Europe, pp. 1686-1691 </td> |
---|
611 | <td>inproceedings</td> |
---|
612 | <td> </td> |
---|
613 | </tr> |
---|
614 | <tr id="bib_Cabodi09Speeding" class="bibtex noshow"> |
---|
615 | <td colspan="7"><b>BibTeX</b>: |
---|
616 | <pre> |
---|
617 | @inproceedings{Cabodi09Speeding, |
---|
618 | author = {G. Cabodi and P. Camurati and L. Garcia and M. Murciano and S. Nocco and S. Quer}, |
---|
619 | title = {Speeding up Model Checking by Exploiting Explicit and Hidden Verification Constraints}, |
---|
620 | booktitle = {DATE '09: Proceedings of the conference on Design, Automation and Test in Europe}, |
---|
621 | year = {2009}, |
---|
622 | pages = {1686-1691} |
---|
623 | } |
---|
624 | </pre></td> |
---|
625 | </tr> |
---|
626 | <tr id="Cansell2001AbstractionandRefinementofFeatures" class="entry"> |
---|
627 | <td>Cansell, D. & Méry, D. S. Gilmore and M. Ryan (Ed.)</td> |
---|
628 | <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> |
---|
629 | <td>2001</td> |
---|
630 | <td>Language Constructs for Designing Features, pp. 65-84 </td> |
---|
631 | <td>incollection</td> |
---|
632 | <td> </td> |
---|
633 | </tr> |
---|
634 | <tr id="abs_Cansell2001AbstractionandRefinementofFeatures" class="abstract noshow"> |
---|
635 | <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> |
---|
636 | </tr> |
---|
637 | <tr id="bib_Cansell2001AbstractionandRefinementofFeatures" class="bibtex noshow"> |
---|
638 | <td colspan="7"><b>BibTeX</b>: |
---|
639 | <pre> |
---|
640 | @incollection{Cansell2001AbstractionandRefinementofFeatures, |
---|
641 | author = {D.~Cansell and D.~Méry}, |
---|
642 | title = {Abstraction and Refinement of Features}, |
---|
643 | booktitle = {Language Constructs for Designing Features}, |
---|
644 | publisher = {Springer-Verlag}, |
---|
645 | year = {2001}, |
---|
646 | pages = {65--84} |
---|
647 | } |
---|
648 | </pre></td> |
---|
649 | </tr> |
---|
650 | <tr id="DBLP:conf/lics/ClarkeLM89" class="entry"> |
---|
651 | <td>Clarke, E.M., Long, D.E. & McMillan, K.L. </td> |
---|
652 | <td>Compositional Model Checking <p class="infolinks">[<a href="javascript:toggleInfo('DBLP:conf/lics/ClarkeLM89','bibtex')">BibTeX</a>]</p></td> |
---|
653 | <td>1989</td> |
---|
654 | <td>LICS'89: Proceedings of the 4th Annual Symposium on Logic in Computer Science, pp. 353-362 </td> |
---|
655 | <td>inproceedings</td> |
---|
656 | <td> </td> |
---|
657 | </tr> |
---|
658 | <tr id="bib_DBLP:conf/lics/ClarkeLM89" class="bibtex noshow"> |
---|
659 | <td colspan="7"><b>BibTeX</b>: |
---|
660 | <pre> |
---|
661 | @inproceedings{DBLP:conf/lics/ClarkeLM89, |
---|
662 | author = {E.~M.~Clarke and D.~E.~Long and K.~L.~McMillan}, |
---|
663 | title = {Compositional Model Checking}, |
---|
664 | booktitle = {LICS'89: Proceedings of the 4th Annual Symposium on Logic in Computer Science}, |
---|
665 | publisher = {IEEE Computer Society}, |
---|
666 | year = {1989}, |
---|
667 | pages = {353-362} |
---|
668 | } |
---|
669 | </pre></td> |
---|
670 | </tr> |
---|
671 | <tr id="6128043" class="entry"> |
---|
672 | <td>Feng, Y., Veeramani, A., Kanagasabai, R. & Rho, S. </td> |
---|
673 | <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> |
---|
674 | <td>2011</td> |
---|
675 | <td>Services Computing Conference (APSCC), 2011 IEEE Asia-Pacific, pp. 477 -482 </td> |
---|
676 | <td>inproceedings</td> |
---|
677 | <td><a href="http://dx.doi.org/10.1109/APSCC.2011.54">DOI</a> </td> |
---|
678 | </tr> |
---|
679 | <tr id="abs_6128043" class="abstract noshow"> |
---|
680 | <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> |
---|
681 | </tr> |
---|
682 | <tr id="bib_6128043" class="bibtex noshow"> |
---|
683 | <td colspan="7"><b>BibTeX</b>: |
---|
684 | <pre> |
---|
685 | @inproceedings{6128043, |
---|
686 | author = {Yuzhang Feng and Veeramani, A. and Kanagasabai, R. and Seungmin Rho}, |
---|
687 | title = {Automatic Service Composition via Model Checking}, |
---|
688 | booktitle = {Services Computing Conference (APSCC), 2011 IEEE Asia-Pacific}, |
---|
689 | year = {2011}, |
---|
690 | pages = {477 -482}, |
---|
691 | doi = {http://dx.doi.org/10.1109/APSCC.2011.54} |
---|
692 | } |
---|
693 | </pre></td> |
---|
694 | </tr> |
---|
695 | <tr id="jhala01microarchi" class="entry"> |
---|
696 | <td>Jhala, R. & McMillan, K. Alain Finkel Gérard Berry, Hubert Comon (Ed.)</td> |
---|
697 | <td>Microarchitecture Verification by Compositional Model Checking. <p class="infolinks">[<a href="javascript:toggleInfo('jhala01microarchi','bibtex')">BibTeX</a>]</p></td> |
---|
698 | <td>2001</td> |
---|
699 | <td><br/>Vol. 2102CAV'01: Proceedings of the 13th International Conference on Computer Aided Verification, pp. 396-410 </td> |
---|
700 | <td>inproceedings</td> |
---|
701 | <td> </td> |
---|
702 | </tr> |
---|
703 | <tr id="bib_jhala01microarchi" class="bibtex noshow"> |
---|
704 | <td colspan="7"><b>BibTeX</b>: |
---|
705 | <pre> |
---|
706 | @inproceedings{jhala01microarchi, |
---|
707 | author = {Jhala, R. and McMillan, K.L.}, |
---|
708 | title = {Microarchitecture Verification by Compositional Model Checking.}, |
---|
709 | booktitle = {CAV'01: Proceedings of the 13th International Conference on Computer Aided Verification}, |
---|
710 | publisher = {Springer}, |
---|
711 | year = {2001}, |
---|
712 | volume = {2102}, |
---|
713 | pages = {396-410} |
---|
714 | } |
---|
715 | </pre></td> |
---|
716 | </tr> |
---|
717 | <tr id="springerlink:10.1007/978-3-540-68073-4_4" class="entry"> |
---|
718 | <td>Li, J., Sun, X., Xie, F. & Song, X. Hong Mei (Ed.)</td> |
---|
719 | <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> |
---|
720 | <td>2008</td> |
---|
721 | <td><br/>Vol. 5030High Confidence Software Reuse in Large Systems, pp. 39-51 </td> |
---|
722 | <td>incollection</td> |
---|
723 | <td><a href="http://dx.doi.org/10.1007/978-3-540-68073-4_4">URL</a> </td> |
---|
724 | </tr> |
---|
725 | <tr id="bib_springerlink:10.1007/978-3-540-68073-4_4" class="bibtex noshow"> |
---|
726 | <td colspan="7"><b>BibTeX</b>: |
---|
727 | <pre> |
---|
728 | @incollection{springerlink:10.1007/978-3-540-68073-4_4, |
---|
729 | author = {Li, Juncao and Sun, Xiuli and Xie, Fei and Song, Xiaoyu}, |
---|
730 | title = {Component-Based Abstraction and Refinement}, |
---|
731 | booktitle = {High Confidence Software Reuse in Large Systems}, |
---|
732 | publisher = {Springer Berlin / Heidelberg}, |
---|
733 | year = {2008}, |
---|
734 | volume = {5030}, |
---|
735 | pages = {39-51}, |
---|
736 | note = {10.1007/978-3}, |
---|
737 | url = {http://dx.doi.org/10.1007/978-3-540-68073-4_4} |
---|
738 | } |
---|
739 | </pre></td> |
---|
740 | </tr> |
---|
741 | <tr id="springerlink:10.1007/978-3-642-16901-4_15" class="entry"> |
---|
742 | <td>Lomuscio, A., Strulo, B., Walker, N. & Wu, P. Jin Dong and Huibiao Zhu (Ed.)</td> |
---|
743 | <td>Assume-Guarantee Reasoning with Local Specifications <p class="infolinks">[<a href="javascript:toggleInfo('springerlink:10.1007/978-3-642-16901-4_15','abstract')">Abstract</a>] [<a href="javascript:toggleInfo('springerlink:10.1007/978-3-642-16901-4_15','bibtex')">BibTeX</a>]</p></td> |
---|
744 | <td>2010</td> |
---|
745 | <td><br/>Vol. 6447Formal Methods and Software Engineering, pp. 204-219 </td> |
---|
746 | <td>incollection</td> |
---|
747 | <td><a href="http://dx.doi.org/10.1007/978-3-642-16901-4_15">URL</a> </td> |
---|
748 | </tr> |
---|
749 | <tr id="abs_springerlink:10.1007/978-3-642-16901-4_15" class="abstract noshow"> |
---|
750 | <td colspan="7"><b>Abstract</b>: 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.</td> |
---|
751 | </tr> |
---|
752 | <tr id="bib_springerlink:10.1007/978-3-642-16901-4_15" class="bibtex noshow"> |
---|
753 | <td colspan="7"><b>BibTeX</b>: |
---|
754 | <pre> |
---|
755 | @incollection{springerlink:10.1007/978-3-642-16901-4_15, |
---|
756 | author = {Lomuscio, Alessio and Strulo, Ben and Walker, Nigel and Wu, Peng}, |
---|
757 | title = {Assume-Guarantee Reasoning with Local Specifications}, |
---|
758 | booktitle = {Formal Methods and Software Engineering}, |
---|
759 | publisher = {Springer Berlin / Heidelberg}, |
---|
760 | year = {2010}, |
---|
761 | volume = {6447}, |
---|
762 | pages = {204-219}, |
---|
763 | note = {10.1007/978-3-642-16901-4_15}, |
---|
764 | url = {http://dx.doi.org/10.1007/978-3-642-16901-4_15} |
---|
765 | } |
---|
766 | </pre></td> |
---|
767 | </tr> |
---|
768 | <tr id="long93thesis" class="entry"> |
---|
769 | <td>Long, D.E. </td> |
---|
770 | <td>Model Checking, Abstraction, and Compositional Verification <p class="infolinks">[<a href="javascript:toggleInfo('long93thesis','bibtex')">BibTeX</a>]</p></td> |
---|
771 | <td>1993</td> |
---|
772 | <td><i>School</i>: Carnegie Mellon University </td> |
---|
773 | <td>phdthesis</td> |
---|
774 | <td> </td> |
---|
775 | </tr> |
---|
776 | <tr id="bib_long93thesis" class="bibtex noshow"> |
---|
777 | <td colspan="7"><b>BibTeX</b>: |
---|
778 | <pre> |
---|
779 | @phdthesis{long93thesis, |
---|
780 | author = {D.~E.~Long}, |
---|
781 | title = {Model Checking, Abstraction, and Compositional Verification}, |
---|
782 | school = {Carnegie Mellon University}, |
---|
783 | year = {1993} |
---|
784 | } |
---|
785 | </pre></td> |
---|
786 | </tr> |
---|
787 | <tr id="mcmillan98tomasulo" class="entry"> |
---|
788 | <td>McMillan, K. Moshe Y. Vardi Alan J. Hu (Ed.)</td> |
---|
789 | <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> |
---|
790 | <td>1998</td> |
---|
791 | <td><br/>Vol. 1427CAV'98: Proceddings of the 10th International Conference on Computer Aided Verification, pp. 110-121 </td> |
---|
792 | <td>inproceedings</td> |
---|
793 | <td> </td> |
---|
794 | </tr> |
---|
795 | <tr id="bib_mcmillan98tomasulo" class="bibtex noshow"> |
---|
796 | <td colspan="7"><b>BibTeX</b>: |
---|
797 | <pre> |
---|
798 | @inproceedings{mcmillan98tomasulo, |
---|
799 | author = {K.L.~McMillan}, |
---|
800 | title = {Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking.}, |
---|
801 | booktitle = {CAV'98: Proceddings of the 10th International Conference on Computer Aided Verification}, |
---|
802 | publisher = {Springer}, |
---|
803 | year = {1998}, |
---|
804 | volume = {1427}, |
---|
805 | pages = {110-121} |
---|
806 | } |
---|
807 | </pre></td> |
---|
808 | </tr> |
---|
809 | <tr id="mcmillan00methodology" class="entry"> |
---|
810 | <td>McMillan, K. </td> |
---|
811 | <td>A Methodology for Hardware Verification Using Compositional Model Checking <p class="infolinks">[<a href="javascript:toggleInfo('mcmillan00methodology','bibtex')">BibTeX</a>]</p></td> |
---|
812 | <td>2000</td> |
---|
813 | <td>Science of Computer Programming<br/>Vol. 37(1-3), pp. 279-309 </td> |
---|
814 | <td>article</td> |
---|
815 | <td><a href="citeseer.ist.psu.edu/mcmillan99methodology.html">URL</a> </td> |
---|
816 | </tr> |
---|
817 | <tr id="bib_mcmillan00methodology" class="bibtex noshow"> |
---|
818 | <td colspan="7"><b>BibTeX</b>: |
---|
819 | <pre> |
---|
820 | @article{mcmillan00methodology, |
---|
821 | author = {K.L. McMillan}, |
---|
822 | title = {A Methodology for Hardware Verification Using Compositional Model Checking}, |
---|
823 | journal = {Science of Computer Programming}, |
---|
824 | year = {2000}, |
---|
825 | volume = {37}, |
---|
826 | number = {1--3}, |
---|
827 | pages = {279--309}, |
---|
828 | url = {citeseer.ist.psu.edu/mcmillan99methodology.html} |
---|
829 | } |
---|
830 | </pre></td> |
---|
831 | </tr> |
---|
832 | <tr id="DBLP:conf/cav/McMillan97" class="entry"> |
---|
833 | <td>McMillan, K.L. Orna Grumberg (Ed.)</td> |
---|
834 | <td>A Compositional Rule for Hardware Design Refinement. <p class="infolinks">[<a href="javascript:toggleInfo('DBLP:conf/cav/McMillan97','bibtex')">BibTeX</a>]</p></td> |
---|
835 | <td>1997</td> |
---|
836 | <td><br/>Vol. 1254CAV'97: Proceedings of the 9th International Conference on Computer Aided Verification, pp. 24-35 </td> |
---|
837 | <td>inproceedings</td> |
---|
838 | <td> </td> |
---|
839 | </tr> |
---|
840 | <tr id="bib_DBLP:conf/cav/McMillan97" class="bibtex noshow"> |
---|
841 | <td colspan="7"><b>BibTeX</b>: |
---|
842 | <pre> |
---|
843 | @inproceedings{DBLP:conf/cav/McMillan97, |
---|
844 | author = {Kenneth L. McMillan}, |
---|
845 | title = {A Compositional Rule for Hardware Design Refinement.}, |
---|
846 | booktitle = {CAV'97: Proceedings of the 9th International Conference on Computer Aided Verification}, |
---|
847 | publisher = {Springer}, |
---|
848 | year = {1997}, |
---|
849 | volume = {1254}, |
---|
850 | pages = {24-35} |
---|
851 | } |
---|
852 | </pre></td> |
---|
853 | </tr> |
---|
854 | <tr id="peng02thesis" class="entry"> |
---|
855 | <td>Peng, H. </td> |
---|
856 | <td>Improving Compositional Verification through Environment Synthesis and Syntactic Model Reduction <p class="infolinks">[<a href="javascript:toggleInfo('peng02thesis','bibtex')">BibTeX</a>]</p></td> |
---|
857 | <td>2002</td> |
---|
858 | <td><i>School</i>: Dept. of Electrical and Computer Engenering, Concordia University, Montreal, Quebec, Canada </td> |
---|
859 | <td>phdthesis</td> |
---|
860 | <td> </td> |
---|
861 | </tr> |
---|
862 | <tr id="bib_peng02thesis" class="bibtex noshow"> |
---|
863 | <td colspan="7"><b>BibTeX</b>: |
---|
864 | <pre> |
---|
865 | @phdthesis{peng02thesis, |
---|
866 | author = {H.~Peng}, |
---|
867 | title = {Improving Compositional Verification through Environment Synthesis and Syntactic Model Reduction}, |
---|
868 | school = {Dept. of Electrical and Computer Engenering, Concordia University, Montreal, Quebec, Canada}, |
---|
869 | year = {2002} |
---|
870 | } |
---|
871 | </pre></td> |
---|
872 | </tr> |
---|
873 | <tr id="peng02tableau" class="entry"> |
---|
874 | <td>Peng, H., Mokhtari, Y. & Tahar, S. </td> |
---|
875 | <td>Environment Synthesis for Compositional Model Checking. <p class="infolinks">[<a href="javascript:toggleInfo('peng02tableau','bibtex')">BibTeX</a>]</p></td> |
---|
876 | <td>2002</td> |
---|
877 | <td>ICCD'02: Proceedings of the 20th International Conference on Computer Design, pp. 70- </td> |
---|
878 | <td>inproceedings</td> |
---|
879 | <td> </td> |
---|
880 | </tr> |
---|
881 | <tr id="bib_peng02tableau" class="bibtex noshow"> |
---|
882 | <td colspan="7"><b>BibTeX</b>: |
---|
883 | <pre> |
---|
884 | @inproceedings{peng02tableau, |
---|
885 | author = {H.~Peng and Y.~Mokhtari and S.~Tahar}, |
---|
886 | title = {Environment Synthesis for Compositional Model Checking.}, |
---|
887 | booktitle = {ICCD'02: Proceedings of the 20th International Conference on Computer Design}, |
---|
888 | publisher = {IEEE Computer Society}, |
---|
889 | year = {2002}, |
---|
890 | pages = {70-} |
---|
891 | } |
---|
892 | </pre></td> |
---|
893 | </tr> |
---|
894 | <tr id="Tripakis201" class="entry"> |
---|
895 | <td>Tripakis, S., Andrade, H., Ghosal, A., Limaye, R., Ravindran, K., Wang, G., Yang, G., Kormerup, J. & Wong, I. </td> |
---|
896 | <td>Correct and non-defensive glue design using abstract models <p class="infolinks">[<a href="javascript:toggleInfo('Tripakis201','abstract')">Abstract</a>] [<a href="javascript:toggleInfo('Tripakis201','bibtex')">BibTeX</a>]</p></td> |
---|
897 | <td>2011</td> |
---|
898 | <td>Proceedings of the seventh IEEE/ACM/IFIP international conference on Hardware/software codesign and system synthesis, pp. 59-68 </td> |
---|
899 | <td>inproceedings</td> |
---|
900 | <td><a href="http://doi.acm.org/10.1145/2039370.2039382">DOI</a> <a href="http://doi.acm.org/10.1145/2039370.2039382">URL</a> </td> |
---|
901 | </tr> |
---|
902 | <tr id="abs_Tripakis201" class="abstract noshow"> |
---|
903 | <td colspan="7"><b>Abstract</b>: 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.<p>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. </td> |
---|
904 | </tr> |
---|
905 | <tr id="bib_Tripakis201" class="bibtex noshow"> |
---|
906 | <td colspan="7"><b>BibTeX</b>: |
---|
907 | <pre> |
---|
908 | @inproceedings{Tripakis201, |
---|
909 | 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}, |
---|
910 | title = {Correct and non-defensive glue design using abstract models}, |
---|
911 | booktitle = {Proceedings of the seventh IEEE/ACM/IFIP international conference on Hardware/software codesign and system synthesis}, |
---|
912 | publisher = {ACM}, |
---|
913 | year = {2011}, |
---|
914 | pages = {59--68}, |
---|
915 | url = {http://doi.acm.org/10.1145/2039370.2039382}, |
---|
916 | doi = {http://doi.acm.org/10.1145/2039370.2039382} |
---|
917 | } |
---|
918 | </pre></td> |
---|
919 | </tr> |
---|
920 | <tr id="xie03verified" class="entry"> |
---|
921 | <td>Xie, F. & Browne, J. </td> |
---|
922 | <td>Verified Systems by Composition from Verified Components <p class="infolinks">[<a href="javascript:toggleInfo('xie03verified','bibtex')">BibTeX</a>]</p></td> |
---|
923 | <td>2003</td> |
---|
924 | <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 </td> |
---|
925 | <td>inproceedings</td> |
---|
926 | <td><a href="http://doi.acm.org/10.1145/940071.940109">DOI</a> </td> |
---|
927 | </tr> |
---|
928 | <tr id="bib_xie03verified" class="bibtex noshow"> |
---|
929 | <td colspan="7"><b>BibTeX</b>: |
---|
930 | <pre> |
---|
931 | @inproceedings{xie03verified, |
---|
932 | author = {F.~Xie and J.C.~Browne}, |
---|
933 | title = {Verified Systems by Composition from Verified Components}, |
---|
934 | 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}, |
---|
935 | publisher = {ACM Press}, |
---|
936 | year = {2003}, |
---|
937 | pages = {277--286}, |
---|
938 | doi = {http://doi.acm.org/10.1145/940071.940109} |
---|
939 | } |
---|
940 | </pre></td> |
---|
941 | </tr> |
---|
942 | <tr id="5374376" class="entry"> |
---|
943 | <td>Zheng, H., Yao, H. & Yoneda, T. </td> |
---|
944 | <td>Modular Model Checking of Large Asynchronous Designs with Efficient Abstraction Refinement <p class="infolinks">[<a href="javascript:toggleInfo('5374376','abstract')">Abstract</a>] [<a href="javascript:toggleInfo('5374376','review')">Review</a>] [<a href="javascript:toggleInfo('5374376','bibtex')">BibTeX</a>]</p></td> |
---|
945 | <td>2010</td> |
---|
946 | <td>Computers, IEEE Transactions on<br/>Vol. 59(4), pp. 561 -573 </td> |
---|
947 | <td>article</td> |
---|
948 | <td><a href="http://dx.doi.org/10.1109/TC.2009.187">DOI</a> </td> |
---|
949 | </tr> |
---|
950 | <tr id="abs_5374376" class="abstract noshow"> |
---|
951 | <td colspan="7"><b>Abstract</b>: 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.</td> |
---|
952 | </tr> |
---|
953 | <tr id="rev_5374376" class="review noshow"> |
---|
954 | <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> |
---|
955 | </tr> |
---|
956 | <tr id="bib_5374376" class="bibtex noshow"> |
---|
957 | <td colspan="7"><b>BibTeX</b>: |
---|
958 | <pre> |
---|
959 | @article{5374376, |
---|
960 | author = {Hao Zheng and Haiqiong Yao and Yoneda, T.}, |
---|
961 | title = {Modular Model Checking of Large Asynchronous Designs with Efficient Abstraction Refinement}, |
---|
962 | journal = {Computers, IEEE Transactions on}, |
---|
963 | year = {2010}, |
---|
964 | volume = {59}, |
---|
965 | number = {4}, |
---|
966 | pages = {561 -573}, |
---|
967 | doi = {http://dx.doi.org/10.1109/TC.2009.187} |
---|
968 | } |
---|
969 | </pre></td> |
---|
970 | </tr> |
---|
971 | <tr id="DBLP:conf/compos/1997" class="entry"> |
---|
972 | <td> Willem P. de Roever and Hans Langmaack and Amir Pnueli (Ed.)</td> |
---|
973 | <td>Compositionality: The Significant Difference, International Symposium, COMPOS'97, Bad Malente, Germany, September 8-12, 1997. Revised Lectures <p class="infolinks">[<a href="javascript:toggleInfo('DBLP:conf/compos/1997','bibtex')">BibTeX</a>]</p></td> |
---|
974 | <td>1998</td> |
---|
975 | <td><br/>Vol. 1536COMPOS </td> |
---|
976 | <td>proceedings</td> |
---|
977 | <td> </td> |
---|
978 | </tr> |
---|
979 | <tr id="bib_DBLP:conf/compos/1997" class="bibtex noshow"> |
---|
980 | <td colspan="7"><b>BibTeX</b>: |
---|
981 | <pre> |
---|
982 | @proceedings{DBLP:conf/compos/1997,, |
---|
983 | title = {Compositionality: The Significant Difference, International Symposium, COMPOS'97, Bad Malente, Germany, September 8-12, 1997. Revised Lectures}, |
---|
984 | booktitle = {COMPOS}, |
---|
985 | publisher = {Springer}, |
---|
986 | year = {1998}, |
---|
987 | volume = {1536} |
---|
988 | } |
---|
989 | </pre></td> |
---|
990 | </tr> |
---|
991 | </tbody> |
---|
992 | </table> |
---|
993 | |
---|
994 | <p> |
---|
995 | <small>Created by <a href="http://jabref.sourceforge.net">JabRef</a> on 07/03/2012.</small> |
---|
996 | </p> |
---|
997 | |
---|
998 | </body> |
---|
999 | </html> |
---|
1000 | |
---|
1001 | <!-- File generated by JabRef ; Export Filter written by Mark Schenk --> |
---|