3 ms·

I've looked into formal verification in the past and from what I've seen it boils down to either annotating your source code with constraints that are then chec

I've looked into formal verification in the past and from what I've seen it boils down to either annotating your source code with constraints that are then checked to verify the software does what you say it does, or you write a specification in a separate language that is supposed to represent the intended functionality of the system and then you write the system such that it matches the specification. The problem in both these cases is that "formally verified" just means that you verify your specification doesn't violate anything you've said it shouldn't, but you might have written your specification incorrectly, or your specification might not match what you say it matches, which then makes the whole thing irrelevant. That's not to say there's no value in formal verification, but I tend to see the value more in verifying some tricky protocol or very concurrent thing works properly (because these often have subtle bugs that are very hard to detect from inspection), rather than as a way to verify that your whole system works. Plus for autopilot, how would you even specify that? The problem is too big and ill-defined to be specified in any way that would be amenable to verification. Of course, individual sub-problems could be verified but that's no guarantee that the system as a whole works.

vsskanth 7y ago
is it not possible to specify global constraints and verify the code against that ? (ex. minimum 2 sensors should give an estimate of each attribute, vehicle should not be able to crash into anything, hierarchical control modes for sensor failure, etc.)
- jeffreyrogers 7y ago
  You can definitely do the first of those examples and probably the last of the examples, but the middle one (vehicle should not be able to crash into anything) is really hard. How do you prove the vehicle can't crash into anything? What do you specify in code to ensure that? I guarantee whatever specification you make I can come up with an edge case that it won't handle. That's the main problem with specification, not that it doesn't work, but that we don't know enough about what a solution would look like to fully specify it. And just to dive into this a little more, let's say the first example you gave fails, and we have one sensor saying something is 10m in front of us and the other saying there's nothing for 100m, what do we do in this situation? Well, it depends on the context, maybe the one sensor is picking up a bit of retread tire in the middle of the lane and we can just drive over it, or maybe the other sensor is malfunctioning and there's actually a bear in the road. I don't think there is an easy answer to what to do in general just given the sensor state.
  - vsskanth 7y ago
    Thank you

vsskanth 7y ago

is it not possible to specify global constraints and verify the code against that ? (ex. minimum 2 sensors should give an estimate of each attribute, vehicle should not be able to crash into anything, hierarchical control modes for sensor failure, etc.)

jeffreyrogers 7y ago
You can definitely do the first of those examples and probably the last of the examples, but the middle one (vehicle should not be able to crash into anything) is really hard. How do you prove the vehicle can't crash into anything? What do you specify in code to ensure that? I guarantee whatever specification you make I can come up with an edge case that it won't handle. That's the main problem with specification, not that it doesn't work, but that we don't know enough about what a solution would look like to fully specify it. And just to dive into this a little more, let's say the first example you gave fails, and we have one sensor saying something is 10m in front of us and the other saying there's nothing for 100m, what do we do in this situation? Well, it depends on the context, maybe the one sensor is picking up a bit of retread tire in the middle of the lane and we can just drive over it, or maybe the other sensor is malfunctioning and there's actually a bear in the road. I don't think there is an easy answer to what to do in general just given the sensor state.
- vsskanth 7y ago
  Thank you