So at one of my older jobs, we worked primarily with C code that ran on a mini linux box inside a plane, and interfaces with a sensor pacakge. We wanted to make sure that the software was 100% correct cause any errors would mean an aborted flight test
We basically ended up creating a tool+language spec that would let us define the mapping of input to output sequences. We wrote it in such a way where we sat with scientists and pretty much mapped all the possible cases that they could think of for valid inputs and what the code should produce.
Then this tool would basically write automated tests for us, in such a way as to not only test correct behavior, but also do combinations of inputs out of order, fuzz testing, and so on. We ended up making it also check memory state, to ensure that there was no memory leaks, and analyze the memory space for required data or data that should not be there.
In the end, whenever someone was developing anything for this software, they would basically just run the tests, and it would be very good at catching possible errors, mostly on the negative side (i.e for a fuzzed input, it would result in an output that should be an error).
We could have done the same thing with a typed language, but it would have to be very strict typing to the point of something like CoQ, and it would have taken us probably the same amount of time to write that.
Hey, that's awesome. Seems like a great case for verifying things that way! I'm thinking of different cases I think, where you've got something like a distributed system or a web application and it's just harder to fuzz. But I agree, that seems a lot more practical than formally verifying it when that's the kind of testing you need.
We basically ended up creating a tool+language spec that would let us define the mapping of input to output sequences. We wrote it in such a way where we sat with scientists and pretty much mapped all the possible cases that they could think of for valid inputs and what the code should produce.
Then this tool would basically write automated tests for us, in such a way as to not only test correct behavior, but also do combinations of inputs out of order, fuzz testing, and so on. We ended up making it also check memory state, to ensure that there was no memory leaks, and analyze the memory space for required data or data that should not be there.
In the end, whenever someone was developing anything for this software, they would basically just run the tests, and it would be very good at catching possible errors, mostly on the negative side (i.e for a fuzzed input, it would result in an output that should be an error).
We could have done the same thing with a typed language, but it would have to be very strict typing to the point of something like CoQ, and it would have taken us probably the same amount of time to write that.