<XML><RECORDS><RECORD><REFERENCE_TYPE>3</REFERENCE_TYPE><REFNUM>9144</REFNUM><AUTHORS><AUTHOR>Sharma,O.</AUTHOR><AUTHOR>Lewis,J.</AUTHOR><AUTHOR>Miller,A.</AUTHOR><AUTHOR>Dearle,A.</AUTHOR><AUTHOR>Balasubramaniam,D.</AUTHOR><AUTHOR>Morrison,R.</AUTHOR><AUTHOR>Sventek,J.</AUTHOR></AUTHORS><YEAR>2009</YEAR><TITLE>Towards Verifying Correctness of Wireless Sensor Network Applications using Insense and Spin</TITLE><PLACE_PUBLISHED>Proceedings of the 16th Spin workshop (Spin'09), Lecture Notes in Computing Science 5758</PLACE_PUBLISHED><PUBLISHER>Springer</PUBLISHER><PAGES>223--240</PAGES><ISBN>978-3-642-02651-5</ISBN><LABEL>Sharma:2009:9144</LABEL><KEYWORDS><KEYWORD>Insense</KEYWORD></KEYWORDS<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 an 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.</ABSTRACT><NOTES>To appear</NOTES></RECORD></RECORDS></XML>