Database Reference
In-Depth Information
Unfortunately, when applied to sensor networks, today's formal meth-
ods tools for embedded software are greatly hampered by the dimention-
ality explosion that arises from massive concurrency. Different event
interleavings at different nodes can generate an exponential number of
possible states, making analysis intractable. While a substantial amount
of work does address formal correctness assurances in sensor network sys-
tems, current solutions fall short of a complete correctness proof. For
example, they might feature
approximate
state coverage, focus on ver-
ifying
individual
components, consider
single-node
systems, or
simplify
semantics
of communication and sensing.
To appreciate the need for
run-time
troubleshooting, which is the
topic of this survey, it is informative to consider the limitations of
present formal
pre-run-time
approaches. A significant set of pre-run-
time tools focus on checking models of application code written for pop-
ular sensor network operating systems, such as TinyOS [59], to ensure
that certain desirable properties are never violated. Early work [91, 72]
sought abstract high-level models for TinyOS applications. The corre-
spondence between these models and actual software implementation,
however, would remain to be verified. Formal method-based solutions
were also proposed to verify individual components or protocols, such as
security protocols in [42] (expressed in the HLPSL [16] high-level formal
specification language), sensor coverage protocols in [74] (expressed in
real-time Maude [73]), and others [24]. To reduce the searched state
space, approximations and incomplete coverage were also considered.
For example, T-check [60] is a model checker that explores a simplified
search space (of a protocol simulation), in order to check safety and live-
ness properties. KleeNet [80, 79] takes the alternative approach of sym-
bolic execution, where given symbolic inputs, all paths of a distributed
program are traversed in search for bugs. However, not all combinations
of possible timings of distributed race conditions are considered.
More recent approaches verify safety assersions of actual complete ap-
plication code [11, 100, 71]. For example, recent work on compile-time
checking [100] verifies distributed sensor network programs directly in
NesC [31] (a common sensor network programming language), given
a simplified communication and sensing model. Another compile-time
checker, called Anquiro [71], maps C programs written for Contiki [25]
(also a popular sensor network operating system) to a state space where
they can be statically verified. While these systems can uncover bugs in
real code, a general problem with them is that the state space grows ex-
ponentially with the amount of communication and race conditions. The
intractability of comprehensive solutions for uncovering sensor network
bugs at design time increases the importance of
run-time troubleshooting
