The research is good - range tracking is something that ever verification model should do.
But reading words "Arduino" and "safety critical" in the same sentence jars me every time. Yes, Arduino ecosystem is large, and it is very easy to get started with it. But it's precisely for this reason it's full of awful quality code and bad practices. Most of the libraries have no error checking, no data validation and use APIs which will happily provide invalid data.
I used esbmc, and it was better than cbmc. I also used it in 8/16 bit firmware, because there is where it shines. Small and easy to verify.
The libraries were bad, yes, so I had to fix it. No big deal. The device has to run for years without update, so it needs verification.
The research is good - range tracking is something that ever verification model should do.
But reading words "Arduino" and "safety critical" in the same sentence jars me every time. Yes, Arduino ecosystem is large, and it is very easy to get started with it. But it's precisely for this reason it's full of awful quality code and bad practices. Most of the libraries have no error checking, no data validation and use APIs which will happily provide invalid data.
I used esbmc, and it was better than cbmc. I also used it in 8/16 bit firmware, because there is where it shines. Small and easy to verify. The libraries were bad, yes, so I had to fix it. No big deal. The device has to run for years without update, so it needs verification.