Skip to Main content Skip to Navigation
Conference papers

Formal Verification of Netlog Protocols

Meixian Chen 1 Jean-François Monin 2, 3
1 BASICS
BASICS - BASICS
2 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : Data centric languages, such as recursive rule based languages, have been proposed to program distributed applications over networks. They greatly simplify the code, while still admitting efficient distributed execution, including on sensor networks. From previous work \cite{discotec11}, we know that they also provide a promising approach to another tough issue about distributed protocols: their formal verification. Indeed, we can take advantage of their data centric orientation, which allows us to explicitly handle global structures such as the topology of the network. We illustrate here our approach on two non-trivial protocols and discuss its Coq implementation.
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/hal-00733634
Contributor : Jean-François Monin <>
Submitted on : Wednesday, September 19, 2012 - 3:37:03 PM
Last modification on : Friday, November 6, 2020 - 4:10:56 AM
Long-term archiving on: : Thursday, December 20, 2012 - 3:46:04 AM

File

tase.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00733634, version 1

Collections

Citation

Meixian Chen, Jean-François Monin. Formal Verification of Netlog Protocols. TASE, Jul 2012, Beijing, China. ⟨hal-00733634⟩

Share

Metrics

Record views

438

Files downloads

409