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

doi:10.1007/978-3-642-02652-2_19

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

School of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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 language	English
Title of host publication	Model Checking Software
Subtitle of host publication	16th International SPIN Workshop, Grenoble, France, June 26-28, 2009, Proceedings
Editors	C. S. Pasareanu
Publisher	Springer
Pages	223-240
Number of pages	18
ISBN (Electronic)	978-3-642-02652-2
ISBN (Print)	978-3-642-02651-5
DOIs	https://doi.org/10.1007/978-3-642-02652-2_19
Publication status	Published - 2009
Event	16th International SPIN Workshop on Model Checking in Software - Grenoble, France Duration: 26 Jun 2009 → 28 Jun 2009

Publication series

Name	Lecture Notes in Computer Science
Volume	5578
ISSN (Print)	0302-9743

Conference

Conference	16th International SPIN Workshop on Model Checking in Software
Country/Territory	France
City	Grenoble
Period	26/06/09 → 28/06/09

Keywords

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

Access to Document

10.1007/978-3-642-02652-2_19

SPIN-2009-Paper
(c)2010 Springer-Verlag. The original publication is available at www.springerlink.com
Submitted manuscript, 359 KB

EP/C014782/1: Design, Implementation and Adaptation of Sensor Networks through Multi- Dimensional Co-Design
Morrison, R. (PI)
EPSRC
1/10/05 → 31/03/09
Project: Standard

Cite this

Sharma, O., Lewis, J. P., Miller, A., Dearle, A., Balasubramaniam, D., Morrison, R., & Sventek, J. (2009). Towards verifying correctness of wireless sensor network applications using Insense and Spin. In C. S. Pasareanu (Ed.), Model Checking Software: 16th International SPIN Workshop, Grenoble, France, June 26-28, 2009, Proceedings (pp. 223-240). (Lecture Notes in Computer Science; Vol. 5578). Springer. https://doi.org/10.1007/978-3-642-02652-2_19

@inproceedings{bf44e82af10142af915aa9e332514229,

title = "Towards verifying correctness of wireless sensor network applications using Insense and Spin",

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.",

keywords = "Concurrency, Distributed systems, Formal Modelling, Wireless Sensor Networks, State concurrent systems, Automatic verification, Model",

author = "Oliver Sharma and Lewis, {Jonathan Peter} and Alice Miller and Alan Dearle and Dharini Balasubramaniam and Ronald Morrison and Joe Sventek",

year = "2009",

doi = "10.1007/978-3-642-02652-2_19",

language = "English",

isbn = "978-3-642-02651-5 ",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "223--240",

editor = "{Pasareanu }, {C. S.}",

booktitle = "Model Checking Software",

address = "Netherlands",

note = "16th International SPIN Workshop on Model Checking in Software ; Conference date: 26-06-2009 Through 28-06-2009",

}

Sharma, O, Lewis, JP, Miller, A, Dearle, A , Balasubramaniam, D , Morrison, R & Sventek, J 2009, Towards verifying correctness of wireless sensor network applications using Insense and Spin. in CS Pasareanu (ed.), Model Checking Software: 16th International SPIN Workshop, Grenoble, France, June 26-28, 2009, Proceedings. Lecture Notes in Computer Science, vol. 5578, Springer, pp. 223-240, 16th International SPIN Workshop on Model Checking in Software , Grenoble, France, 26/06/09. https://doi.org/10.1007/978-3-642-02652-2_19

Towards verifying correctness of wireless sensor network applications using Insense and Spin. / Sharma, Oliver; Lewis, Jonathan Peter; Miller, Alice et al.
Model Checking Software: 16th International SPIN Workshop, Grenoble, France, June 26-28, 2009, Proceedings. ed. / C. S. Pasareanu . Springer, 2009. p. 223-240 (Lecture Notes in Computer Science; Vol. 5578).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

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

AU - Sharma, Oliver

AU - Lewis, Jonathan Peter

AU - Miller, Alice

AU - Dearle, Alan

AU - Balasubramaniam, Dharini

AU - Morrison, Ronald

AU - Sventek, Joe

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

KW - Concurrency

KW - Distributed systems

KW - Formal Modelling

KW - Wireless Sensor Networks

KW - State concurrent systems

KW - Automatic verification

KW - Model

U2 - 10.1007/978-3-642-02652-2_19

DO - 10.1007/978-3-642-02652-2_19

M3 - Conference contribution

SN - 978-3-642-02651-5

T3 - Lecture Notes in Computer Science

SP - 223

EP - 240

BT - Model Checking Software

A2 - Pasareanu , C. S.

PB - Springer

T2 - 16th International SPIN Workshop on Model Checking in Software

Y2 - 26 June 2009 through 28 June 2009

ER -

Sharma O, Lewis JP, Miller A, Dearle A , Balasubramaniam D , Morrison R et al. Towards verifying correctness of wireless sensor network applications using Insense and Spin. In Pasareanu CS, editor, Model Checking Software: 16th International SPIN Workshop, Grenoble, France, June 26-28, 2009, Proceedings. Springer. 2009. p. 223-240. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-02652-2_19

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

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Projects

EP/C014782/1: Design, Implementation and Adaptation of Sensor Networks through Multi- Dimensional Co-Design

Cite this