Software Verification for TinyOS

Doina  Bucur; Marta Kwiatkowska

doi:10.1145/1791212.1791274

Software Verification for TinyOS

Doina Bucur, Marta Kwiatkowska

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-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 language	English
Title of host publication	IPSN '10
Subtitle of host publication	Proceedings of the 9th ACM/IEEE International Conference on Information Processing in Sensor Networks
Place of Publication	New York, NY, USA
Publisher	Association for Computing Machinery
Pages	400-401
Number of pages	2
ISBN (Print)	978-1-60558-988-6
DOIs	https://doi.org/10.1145/1791212.1791274
Publication status	Published - 2010
Externally published	Yes
Event	9th ACM/IEEE International Conference on Information Processing in Sensor Networks, IPSN 2010 - Stockholm, Sweden Duration: 12 Apr 2010 → 15 Apr 2010 Conference number: 9

Conference

Conference	9th ACM/IEEE International Conference on Information Processing in Sensor Networks, IPSN 2010
Abbreviated title	IPSN
Country/Territory	Sweden
City	Stockholm
Period	12/04/10 → 15/04/10

Keywords

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

Access to Document

10.1145/1791212.1791274

Cite this

@inproceedings{358cf65e433642f096c5112d68ac1711,

title = "Software Verification for TinyOS",

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.",

keywords = "MSP430, TinyOS, model checking, reliability, safety, sensor networks, software verification, telos",

author = "Doina Bucur and Marta Kwiatkowska",

year = "2010",

doi = "10.1145/1791212.1791274",

language = "English",

isbn = "978-1-60558-988-6",

pages = "400--401",

booktitle = "IPSN '10",

publisher = "Association for Computing Machinery",

address = "United States",

note = "9th ACM/IEEE International Conference on Information Processing in Sensor Networks, IPSN 2010, IPSN ; Conference date: 12-04-2010 Through 15-04-2010",

}

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. Association for Computing Machinery, New York, NY, USA, pp. 400-401, 9th ACM/IEEE International Conference on Information Processing in Sensor Networks, IPSN 2010, Stockholm, Sweden, 12/04/10. https://doi.org/10.1145/1791212.1791274

Software Verification for TinyOS. / Bucur, Doina ; Kwiatkowska, Marta.
IPSN '10: Proceedings of the 9th ACM/IEEE International Conference on Information Processing in Sensor Networks. New York, NY, USA: Association for Computing Machinery, 2010. p. 400-401.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Software Verification for TinyOS

AU - Bucur, Doina

AU - Kwiatkowska, Marta

N1 - Conference code: 9

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

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

U2 - 10.1145/1791212.1791274

DO - 10.1145/1791212.1791274

M3 - Conference contribution

SN - 978-1-60558-988-6

SP - 400

EP - 401

BT - IPSN '10

PB - Association for Computing Machinery

CY - New York, NY, USA

T2 - 9th ACM/IEEE International Conference on Information Processing in Sensor Networks, IPSN 2010

Y2 - 12 April 2010 through 15 April 2010

ER -

Software Verification for TinyOS

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this