Skip to content

Research at St Andrews

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

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

Author(s)

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

School/Research organisations

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.

Close

Details

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
StatePublished - 2009
Event16th International SPIN Workshop on Model Checking in Software - Grenoble, France

Publication series

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

Conference

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

    Research areas

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

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. A component-based model and language for wireless sensor network applications

    Dearle, A., Balasubramaniam, D., Lewis, J. P. & Morrison, R. Jul 2008 32nd annual IEEE International Computer Software and Applications: COMPSAC 2008, 28 July-1 August 2008, Turku, Finland. IEEE Computer Society, p. 1303-1308 6 p. (IEEE COMPSAC)

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

  2. On the selection of connectivity-based metrics for WSNs using a classification of application behaviour

    Boyd, A., Balasubramaniam, D., Dearle, A. & Morrison, R. 7 Jun 2010 2010 IEEE International Conference on Sensor Networks, Ubiquitous, and Trustworthy Computing: SUTC 2010. IEEE Computer Society, p. 268-275 8 p.

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

  3. An Approach to Extending the Lifetime of Wireless Sensor Networks

    Boyd, A., Balasubramaniam, D., Dearle, A. & Morrison, R. Jun 2008 9th Annual Postgraduate Symposium on The Convergence of Telecommunications, Networking and Broadcasting . Liverpool, UK: PGNet, p. 123-128

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

  4. A composition-based approach to the construction and dynamic reconfiguration of wireless sensor network applications

    Balasubramaniam, D., Dearle, A. & Morrison, R. 2008 Software Composition: 7th International Symposium, SC 2008, Budapest, Hungary, March 29-30, 2008. Proceedings. Pautasso, C. & Tanter, E. (eds.). Springer, Vol. 4954, p. 206-214 9 p. (Lecture Notes in Computer Science; vol. 4954)

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

  5. The Napier88 to the Persistent Abstract Machine Compilation Rules

    Balasubramaniam, D., Brown, A. L., Connor, R. C. H., Cutts, Q. I., Dearle, A., Kirby, G. N. C., Morrison, R., Munro, D. S. & Scheuerl, S. 1994 University of St Andrews.

    Research output: Book/ReportOther report

ID: 6247473