| Presentation | 2014-04-25 Modeling and verification for CCN using a proof assistant Coq Takashi MORISHIMA, Mizuki GOTO, Kazuko TAKAHASHI, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | Content-Centric Networking (CCN) is a communication architecture which was developed on 2009. Communication on CCN is based on the names of objects, rather than on addresses. Although its behavior and performance are explored mainly by simulation, they have not been well-established, and behavioral correctness is required to be verified for its practicel use. In this paper, we create an inductive model for a CCN protocol and implement the maching process undertaken in each node. Then we prove that a node can retrieve the content if and only if the user sends a request when it exists in the network, as one of behavioral correctness. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Coq / CCN / behavioral correctness / network protocol / theorem prover / proof assistant |
| Paper # | CPSY2014-8,DC2014-8 |
| Date of Issue |
| Conference Information | |
| Committee | DC |
|---|---|
| Conference Date | 2014/4/18(1days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | |
| Vice Chair | |
| Secretary | |
| Assistant | |
| Paper Information | |
| Registration To | Dependable Computing (DC) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Modeling and verification for CCN using a proof assistant Coq |
| Sub Title (in English) | |
| Keyword(1) | Coq |
| Keyword(2) | CCN |
| Keyword(3) | behavioral correctness |
| Keyword(4) | network protocol |
| Keyword(5) | theorem prover |
| Keyword(6) | proof assistant |
| 1st Author's Name | Takashi MORISHIMA |
| 1st Author's Affiliation | School of Science and Technology, Kwansei Gakuin University() |
| 2nd Author's Name | Mizuki GOTO |
| 2nd Author's Affiliation | School of Science and Technology, Kwansei Gakuin University |
| 3rd Author's Name | Kazuko TAKAHASHI |
| 3rd Author's Affiliation | School of Science and Technology, Kwansei Gakuin University |
| Date | 2014-04-25 |
| Paper # | CPSY2014-8,DC2014-8 |
| Volume (vol) | vol.114 |
| Number (no) | 22 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |