Compilation of Model and Robot Code

[jchen-cs]

Formally verifying a robot program often requires a model of the hardware and its connections to its environment. However, such models are no longer necessary when compiling code for execution on real hardware. We therefore need a way to distinguish places in code that are modeled for verification purposes, but will receive real data from physical sensors when executing on actual hardware.

To minimize impact on the other compiler components, the proposed solution is as follows:

• Introduce a new construct, modeled(x, y) where x is the model of a sensor and y is the actual implementation. For instance, x could be the kinematic model of a robot that simulates the position of an actuator, while y is the driver code necessary for obtaining the actual value from the robot's sensors.
• To the verifier, modeled(x, y) is equivalent to x (y is ignored)
• When in --robot mode, modeled(x, y) gets compiled to y in the executable.

[jchen-cs]

#59

[jchen-cs]

#57