Abstract | ||
---|---|---|
The applicability of model-checking is often restricted by the size of the considered system. To overcome this limitation, a number of techniques have been investigated. Prominent among these are data independence, abstraction, and compositionality. This paper presents a methodology based on deductive reasoning and model-checking which combines these techniques. As we show, the combination of abstraction and compositionality gives a significant added value to each of them in isolation. We substantiate the approach proving safety of a sliding window protocol of window size 16 using Spin and PVS. |
Year | DOI | Venue |
---|---|---|
1999 | 10.1007/3-540-48234-2_5 | SPIN |
Keywords | Field | DocType |
considered system,deductive reasoning,data independence,window protocol,window size,significant added value,sliding window,model checking | Principle of compositionality,Model checking,Sliding window protocol,Abstraction,Data transmission,Computer science,Algorithm,Added value,Deductive reasoning,Data independence | Conference |
Volume | ISSN | ISBN |
1680 | 0302-9743 | 3-540-66499-8 |
Citations | PageRank | References |
15 | 0.92 | 15 |
Authors | ||
4 |
Name | Order | Citations | PageRank |
---|---|---|---|
Karsten Stahl | 1 | 92 | 4.67 |
Kai Baukus | 2 | 101 | 5.21 |
Yassine Lakhnech | 3 | 913 | 78.50 |
Martin Steffen | 4 | 122 | 10.32 |