Colloquium Computer Science

Title: On Formal Verification for Sensor Software


Abstract:

This talk gives an overview of the field of (formal) software
verification, which is a technique for exhaustively debugging programs
against programming errors such as memory violations, and which
improves on classical simulation. In general, the method works by
automatically translating the program and its specification into a
large mathematical model, which is then inputted into a model checking
tool. When porting this debugging technique for sensor applications
(as in [1], which forms the basis of this talk), the difficulties lie
with (i) being able to automatically extract models out of embedded C,
and (ii) decreasing the resulting program’s state space to shorten
verification times.

[1] On Software Verification for TinyOS, Doina Bucur and Marta
Kwiatkowska, Journal of Software and Systems, Elsevier, to appear,
2011 (http://www.daimi.au.dk/~doina/11-JSS-revision/jss.pdf)