Towards verified programming of embedded devices
Jean-Pierre Talpin1,a, Jean-Joseph Marty1,b, Shravan Narayan2,c, Deian Stefan2,d and Rajesh Gupta2,e
1Inria-Irisa Rennes, France
atalpin@inria.fr
bjean-joseph.marty@inria.fr
2University of California at San Diego La Jolla, CA, USA
csrn002@cs.ucsd.edu
ddeian@cs.ucsd.edu
egupta@cs.ucsd.edu
ABSTRACT
We propose a type-driven approach to building verified safe and correct IoT applications. Today’s IoT applications are plagued with bugs that can cause physical damage. This is largely because developers account for physical constraints using ad-hoc techniques. Accounting for such constrains in a more principled fashion demands reasoning about the composition of all the software and hardware components of the application. Our proposed framework takes a step in this direction by (1) using refinement types to make make physical constraints explicit and (2) imposing an event-driven programing discipline to simplify the reasoning of system-wide properties to that of an event queue. In taking this approach, our framework makes it possible for developers to build verified IoT application by making it a type error for code to violate physical constraints.
Keywords: Formal verification, type and proof theory, program and model analysis, hybrid systems
