Temporal Monitors for TinyOS

Doina Bucur

Temporal Monitors for TinyOS

Doina Bucur

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

Abstract

Networked embedded systems generally have extremely low visibility of system faults. In this paper, we report on experimenting with online, node-local temporal monitors for networked embedded nodes running the TinyOS operating system and programmed in the nesC language. We instrument the original node software to signal asynchronous atomic events to a local nesC component running a runtime verification algorithm; this checks LTL properties automatically translated into deterministic state-machine monitors and encoded in nesC. We focus on quantifying the added (i) memory and (ii) computational overhead of this embedded checker and identify practical upper bounds with runtime checking on mainstream embedded platforms.

Original language	English
Title of host publication	Runtime Verification
Subtitle of host publication	Third International Conference, RV 2012, Istanbul, Turkey, September 25-28, 2012, Revised Selected Papers
Editors	Shaz Qadeer, Serdar Tasiran
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	96-109
Number of pages	14
ISBN (Print)	978-3-642-35632-2
Publication status	Published - 2013
Externally published	Yes
Event	3rd International Conference on Runtime Verification 2012 - Istanbul, Turkey Duration: 25 Sept 2012 → 28 Sept 2012 Conference number: 3 http://runtime-verification.org/

Conference

Conference	3rd International Conference on Runtime Verification 2012
Abbreviated title	RV 2012
Country/Territory	Turkey
City	Istanbul
Period	25/09/12 → 28/09/12
Internet address	http://runtime-verification.org/

Cite this

@inbook{defafd26ddb44b6ea94802e3de9ca295,

title = "Temporal Monitors for TinyOS",

abstract = "Networked embedded systems generally have extremely low visibility of system faults. In this paper, we report on experimenting with online, node-local temporal monitors for networked embedded nodes running the TinyOS operating system and programmed in the nesC language. We instrument the original node software to signal asynchronous atomic events to a local nesC component running a runtime verification algorithm; this checks LTL properties automatically translated into deterministic state-machine monitors and encoded in nesC. We focus on quantifying the added (i) memory and (ii) computational overhead of this embedded checker and identify practical upper bounds with runtime checking on mainstream embedded platforms.",

author = "Doina Bucur",

year = "2013",

language = "English",

isbn = "978-3-642-35632-2",

pages = "96--109",

editor = "Shaz Qadeer and Serdar Tasiran",

booktitle = "Runtime Verification",

publisher = "Springer",

address = "Germany",

note = "3rd International Conference on Runtime Verification 2012, RV 2012 ; Conference date: 25-09-2012 Through 28-09-2012",

url = "http://runtime-verification.org/",

}

TY - CHAP

T1 - Temporal Monitors for TinyOS

AU - Bucur, Doina

N1 - Conference code: 3

PY - 2013

Y1 - 2013

N2 - Networked embedded systems generally have extremely low visibility of system faults. In this paper, we report on experimenting with online, node-local temporal monitors for networked embedded nodes running the TinyOS operating system and programmed in the nesC language. We instrument the original node software to signal asynchronous atomic events to a local nesC component running a runtime verification algorithm; this checks LTL properties automatically translated into deterministic state-machine monitors and encoded in nesC. We focus on quantifying the added (i) memory and (ii) computational overhead of this embedded checker and identify practical upper bounds with runtime checking on mainstream embedded platforms.

AB - Networked embedded systems generally have extremely low visibility of system faults. In this paper, we report on experimenting with online, node-local temporal monitors for networked embedded nodes running the TinyOS operating system and programmed in the nesC language. We instrument the original node software to signal asynchronous atomic events to a local nesC component running a runtime verification algorithm; this checks LTL properties automatically translated into deterministic state-machine monitors and encoded in nesC. We focus on quantifying the added (i) memory and (ii) computational overhead of this embedded checker and identify practical upper bounds with runtime checking on mainstream embedded platforms.

M3 - Chapter

SN - 978-3-642-35632-2

SP - 96

EP - 109

BT - Runtime Verification

A2 - Qadeer, Shaz

A2 - Tasiran, Serdar

PB - Springer

CY - Berlin, Heidelberg

T2 - 3rd International Conference on Runtime Verification 2012

Y2 - 25 September 2012 through 28 September 2012

ER -

Temporal Monitors for TinyOS

Abstract

Conference

Fingerprint

Cite this