Document Type

Conference Proceeding

Publication Date

2014

Publication Title

Runtime Verification

Abstract

Wireless sensor networks (“sensornets”) are highly distributed and concurrent, with program actions bound to external stimuli. They exemplify a system class known as reactive systems, which comprise execution units that have “hidden” layers of control flow. A key obstacle in enabling reactive system developers to rigorously validate their implementations has been the absence of precise software component specifications and tools to assist in leveraging those specifications at runtime. We address this obstacle in three ways: (i) We describe a specification approach tailored for reactive environments and demonstrate its application in the context of sensornets. (ii) We describe the design and implementation of extensions to the popular nesC tool-chain that enable the expression of these specifications and automate the generation of runtime monitors that signal violations, if any. (iii) Finally, we apply the specification approach to a significant collection of the most commonly used software components in the TinyOS distribution and analyze the overhead involved in monitoring their correctness.

Comments

5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Proceedings. Volume 8734 of the series Lecture Notes in Computer Science

This work was supported in part by NSF grants CNS- 0746632, CNS-0745846, and CNS-1126344.

Original Citation

J. Zhai, N. Sridhar and J. O. Hallstrom, "Supporting the specification and runtime validation of asynchronous calling patterns in reactive systems," in Runtime Verification: 5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Proceedings, B. Bonakdarpour and S. A. Smolka, Eds. Cham: Springer International Publishing, 2014, pp. 108-123.

DOI

10.1007/978-3-319-11164-3_10

Version

Postprint

Download

Share

COinS