Skip to content

Research at St Andrews

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

Research output: ResearchConference contribution


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

School/Research organisations


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
Number of pages18
ISBN (Electronic)978-3-642-02652-2
ISBN (Print)978-3-642-02651-5
StatePublished - 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
ISSN (Print)0302-9743


Conference16th International SPIN Workshop on Model Checking in Software

    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: ResearchConference 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: ResearchConference 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: ResearchConference 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: ResearchConference 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: ResearchOther report

ID: 6247473