Name
Abstract | ||
|---|---|---|
In this paper, we present techniques for automated verification of behavioural specifications using hidden algebra. Two non-trivial examples, the Alternating Bit Protocol and a snooping cache coherence protocol, are presented with complete specification code and proof scores for CafeOBJ verification system. The refinement proof based on behavioural coinduction is given for the first example, and the coherence proof based on invariance is given for the second. |
Year | DOI | Venue |
|---|---|---|
1999 | 10.1007/3-540-48118-4_36 | World Congress on Formal Methods |
Keywords | Field | DocType |
complete specification code,alternating bit,behavioural coinduction,coherence proof,cafeobj environment,automated verification,proof score,cache coherence protocol,verifying behavioural specifications,behavioural specification,refinement proof,cafeobj verification system | Specification language,Programming language,Invariant (physics),Object-oriented programming,Hidden algebra,Computer science,Alternating bit protocol,Theoretical computer science,Coherence (physics),Formal verification,Cache coherence | Conference |
Volume | ISSN | ISBN |
1709 | 0302-9743 | 3-540-66588-9 |
Citations | PageRank | References |
1 | 0.35 | 10 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Akira Mori | 1 | 8 | 2.60 |
| Kokichi Futatsugi | 2 | 945 | 111.37 |