Towards verifying correctness of wireless sensor network applications using Insense and Spin

Oliver Sharma, Jonathan Peter Lewis, Alice Miller, Alan Dearle, Dharini Balasubramaniam, Ronald Morrison, Joe Sventek

Research output: Chapter in Book/Report/Conference proceedingConference contribution

16 Citations (Scopus)
8 Downloads (Pure)

Abstract

The design and implementation of wireless sensor network applications often require domain experts, who may lack expertise in software engineering, to produce resource-constrained, concurrent, real-time software without the support of high-level software engineering facilities. The Insense language aims to address this mismatch by allowing the complexities of synchronisation, memory management and event-driven programming to be borne by the language implementation rather than by the programmer. The main contribution of this paper is all initial step towards verifying the correctness of WSN applications with a focus on concurrency. We model part of the synchronisation mechanism of the Insense language implementation using Promela constructs and verify its correctness using SPIN. We demonstrate how a previously published version of the mechanism is shown to be incorrect by SPIN, and give complete verification results for the revised mechanism.

Original languageEnglish
Title of host publicationModel Checking Software
Subtitle of host publication16th International SPIN Workshop, Grenoble, France, June 26-28, 2009, Proceedings
EditorsC. S. Pasareanu
PublisherSpringer
Pages223-240
Number of pages18
ISBN (Electronic)978-3-642-02652-2
ISBN (Print)978-3-642-02651-5
DOIs
Publication statusPublished - 2009
Event16th International SPIN Workshop on Model Checking in Software - Grenoble, France
Duration: 26 Jun 200928 Jun 2009

Publication series

NameLecture Notes in Computer Science
Volume5578
ISSN (Print)0302-9743

Conference

Conference16th International SPIN Workshop on Model Checking in Software
Country/TerritoryFrance
CityGrenoble
Period26/06/0928/06/09

Keywords

  • Concurrency
  • Distributed systems
  • Formal Modelling
  • Wireless Sensor Networks
  • State concurrent systems
  • Automatic verification
  • Model

Fingerprint

Dive into the research topics of 'Towards verifying correctness of wireless sensor network applications using Insense and Spin'. Together they form a unique fingerprint.

Cite this