>> most of the code in critical control systems like ECUs isn't written, it's generated from verifiable models.
I'm not sure what "verifiable models" means here. There are a bunch of people using Simulink to "auto-generate" code for some ECUs. I've used it with great results, and I've seen others do that as well. And yet some people still create horrible things with it just like regular code. But not once did I see anything that sounded like formal verification. That doesn't mean it never happens but the way The Mathworks markets their tools, you'd think some kind of magic is done automatically.
On a related note, I always laugh when Mathworks promotes the ability to compare "simulation" results to that of the "generated code". They call it "software in the loop" testing. This is actually getting their customers to verify that the tools they provide work as advertised.
For that kind of development I'd actually prefer to just shut the simulator off always generate code. Simulation should only ever be for plant models, not control systems you want to actually implement in software.
Oh god. You can check any C-code with Polyspace, I've done that. Most of the warnings Polyspace generates (at the time I did it) are not more significant than style - like checking for MISRA compliance doesn't guarantee a lack of bugs.
To me formal verification has always meant proving correctness in a mathematical sense against some sort of formal specification.
None of that really matters though because AFAIK you can't prove a neural net has been trained "correctly" and doesn't contain errors.
I'm not sure what "verifiable models" means here. There are a bunch of people using Simulink to "auto-generate" code for some ECUs. I've used it with great results, and I've seen others do that as well. And yet some people still create horrible things with it just like regular code. But not once did I see anything that sounded like formal verification. That doesn't mean it never happens but the way The Mathworks markets their tools, you'd think some kind of magic is done automatically.
On a related note, I always laugh when Mathworks promotes the ability to compare "simulation" results to that of the "generated code". They call it "software in the loop" testing. This is actually getting their customers to verify that the tools they provide work as advertised.
For that kind of development I'd actually prefer to just shut the simulator off always generate code. Simulation should only ever be for plant models, not control systems you want to actually implement in software.