{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:51:42Z","timestamp":1750308702869,"version":"3.41.0"},"reference-count":20,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2013,1]]},"abstract":"<jats:p>Wireless sensor networks are an increasingly popular application area for embedded systems. Individual sensor nodes within a network are typically resource-constrained, event-driven, and require a high degree of concurrency. This combination of requirements motivated the development of the widely used TinyOS sensor node operating system. The TinyOS concurrency model is a lightweight nonpreemptive system designed to suit the needs of typical sensor network applications. Although the TinyOS concurrency model is easier to reason about than preemptive threads, it can still give rise to undesirable behavior due to unexpected interleavings of related tasks, or unanticipated preemption by interrupt handlers. To aid TinyOS developers in understanding the behavior of their programs we have developed a technique for using the process algebra Communicating Sequential Processes (CSP) to model the interactions between TinyOS components, and between an application and the TinyOS scheduling and preemption mechanisms. Analysis of the resulting models can help TinyOS developers to discover and diagnose concurrency-related errors in their designs that might otherwise go undetected until after the application has been widely deployed. Such analysis is particularly valuable for the TinyOS components that are used as building blocks for a large number of other applications, since a subtle or sporadic error in a widely deployed building block component could be extremely costly to repair.<\/jats:p>","DOI":"10.1145\/2406336.2406341","type":"journal-article","created":{"date-parts":[[2013,1,29]],"date-time":"2013-01-29T16:20:55Z","timestamp":1359476455000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Modeling and Analysis of TinyOS Sensor Node Firmware"],"prefix":"10.1145","volume":"12","author":[{"given":"Allan I.","family":"McInnes","sequence":"first","affiliation":[{"name":"University of Canterbury"}]}],"member":"320","published-online":{"date-parts":[[2013,1]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1236360.1236382"},{"volume-title":"Proceedings of the Workshop on Formal Approaches to Ubiquitous Systems (FAUSt\u201909)","author":"Bucur D.","key":"e_1_2_1_2_1"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/242223.242257"},{"key":"e_1_2_1_4_1","first-page":"5","article-title":"TinyOS: Operating system design for wireless sensor networks","volume":"23","author":"Culler D. E.","year":"2006","journal-title":"Sensors"},{"key":"e_1_2_1_5_1","unstructured":"Gardiner P. et al. 2005. Failures-Divergences Refinement: FDR2 User Manual. Formal Systems (Europe) Ltd.  Gardiner P. et al. 2005. Failures-Divergences Refinement: FDR2 User Manual . Formal Systems (Europe) Ltd."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/780822.781133"},{"key":"e_1_2_1_7_1","unstructured":"Gay D. Levis P. Culler D. and Brewer E. 2005. nesC 1.2 language reference manual. http:\/\/nescc.cvs.sourceforge.net\/viewvc\/*checkout*\/nescc\/nesc\/doc\/ref.pdf?revision=1.18.  Gay D. Levis P. Culler D. and Brewer E. 2005. nesC 1.2 language reference manual. http:\/\/nescc.cvs.sourceforge.net\/viewvc\/*checkout*\/nescc\/nesc\/doc\/ref.pdf?revision=1.18."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10452-7_18"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPSN.2008.62"},{"key":"e_1_2_1_10_1","unstructured":"Levis P. 2006. TinyOS programming. http:\/\/csl.stanford.edu\/ pal\/pubs\/tinyos-programming.pdf.  Levis P. 2006. TinyOS programming. http:\/\/csl.stanford.edu\/ pal\/pubs\/tinyos-programming.pdf."},{"key":"e_1_2_1_11_1","unstructured":"Levis P. 2007. TinyOS 2.x boot sequence. TinyOS Extension Proposal TEP-107 TinyOS Core Working Group.  Levis P. 2007. TinyOS 2.x boot sequence. TinyOS Extension Proposal TEP-107 TinyOS Core Working Group."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/958491.958506"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Levis P. Madden N. etal 2005. TinyOS: An operating system for sensor networks. In Ambient Intelligence W. Weber J. Rabaey and E. Aarts Eds. Springer 115--148.  Levis P. Madden N. et al. 2005. TinyOS: An operating system for sensor networks. In Ambient Intelligence W. Weber J. Rabaey and E. Aarts Eds. Springer 115--148.","DOI":"10.1007\/3-540-27139-2_7"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECBS.2009.34"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.3390\/s7081447"},{"key":"e_1_2_1_16_1","unstructured":"Roscoe A. W. 1998. The Theory and Practice of Concurrency. Prentice Hall Englewood Cliffs NJ.   Roscoe A. W. 1998. The Theory and Practice of Concurrency . Prentice Hall Englewood Cliffs NJ."},{"key":"e_1_2_1_17_1","unstructured":"Sharp C. 2008. AlarmToTimerC.nc. TinyOS 2.x Source. http:\/\/code.google.com\/p\/tinyos-main\/source\/browse\/trunk\/tos\/lib\/timer\/AlarmToTimerC.nc?r=5108.  Sharp C. 2008. AlarmToTimerC.nc. TinyOS 2.x Source. http:\/\/code.google.com\/p\/tinyos-main\/source\/browse\/trunk\/tos\/lib\/timer\/AlarmToTimerC.nc?r=5108."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.11.012"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1278972.1278996"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/11901914_14"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2406336.2406341","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2406336.2406341","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:13:55Z","timestamp":1750277635000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2406336.2406341"}},"subtitle":["A CSP Approach"],"short-title":[],"issued":{"date-parts":[[2013,1]]},"references-count":20,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,1]]}},"alternative-id":["10.1145\/2406336.2406341"],"URL":"https:\/\/doi.org\/10.1145\/2406336.2406341","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2013,1]]},"assertion":[{"value":"2010-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}