On Formal Verification of Sensor Software
Doina Bucur
Innovation Center for Andvanced Sensors and Sensor Systems (INCAS3)

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. Reference:
[1] On Software Verification for TinyOS, Doina Bucur and Marta Kwiatkowska, Journal of Software and Systems, Elsevier, to appear, 2011, link to the paper

back to the list of talks