Software Verification for TinyOS

Doina Bucur, Marta Kwiatkowska

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

12 Citations (Scopus)

Abstract

We describe the first software tool for the verification of TinyOS 2, MSP430 applications at compile-time. Given assertions upon the state of the sensor node, the tool boundedly explores all program executions and returns to the programmer an error trace leading to any assertion violation. Besides memory-related errors (out-of-bounds arrays, nullpointer dereferences), we verify application-specific assertions, including low-level assertions upon the state of the registers and peripherals.
Original languageEnglish
Title of host publicationIPSN '10
Subtitle of host publicationProceedings of the 9th ACM/IEEE International Conference on Information Processing in Sensor Networks
Place of PublicationNew York, NY, USA
PublisherAssociation for Computing Machinery (ACM)
Pages400-401
Number of pages2
ISBN (Print)978-1-60558-988-6
DOIs
Publication statusPublished - 2010
Externally publishedYes
Event9th ACM/IEEE International Conference on Information Processing in Sensor Networks, IPSN 2010 - Stockholm, Sweden
Duration: 12 Apr 201015 Apr 2010
Conference number: 9

Conference

Conference9th ACM/IEEE International Conference on Information Processing in Sensor Networks, IPSN 2010
Abbreviated titleIPSN
CountrySweden
CityStockholm
Period12/04/1015/04/10

Keywords

  • MSP430, TinyOS, model checking, reliability, safety, sensor networks, software verification, telos

Fingerprint Dive into the research topics of 'Software Verification for TinyOS'. Together they form a unique fingerprint.

  • Cite this

    Bucur, D., & Kwiatkowska, M. (2010). Software Verification for TinyOS. In IPSN '10: Proceedings of the 9th ACM/IEEE International Conference on Information Processing in Sensor Networks (pp. 400-401). New York, NY, USA: Association for Computing Machinery (ACM). https://doi.org/10.1145/1791212.1791274