This talk was given by Cyrille Comar at the recent SPARK User Group. This talk reviews the prominent place and role testing holds in Safety Standards. It compares the strengths and weaknesses of testing with an alternative verification technique based on formal methods. It then explores specific instances where a combination of both approaches makes sense and can bring significant cost savings, without forcing dramatic changes in internal development procedures.
Categories
Open-DO Projects
Contact
info @ open-do.org
2 Comments
To my understanding, Formal verification and testing are complimentary solutions to the verification and validation process. Testing helps to validate that the software is functionally correct and the formal verification tools can check for errors in the implementation. Here is an example of how one such formal verification tool proves code correctness:
http://www.mathworks.com/videos/proving-the-absence-of-run-time-errors-with-polyspace-71970.html
Ram, you’re right that formal verification and testing are complementary, that’s precisely this complementarity that we rely on in the next version of the SPARK technology. You mention PolySpace as a tool that can check for run-time errors in implementations. That’s what static analyzers do indeed, like the one we develop at AdaCore:
http://www.adacore.com/codepeer/
SPARK technology goes one step further, by also allowing you to prove that the intended functionality of pieces of your software is correctly implemented. This requires you to state the intended functionality in contracts (preconditions and postconditions) that the tool then attempts to prove wrt your implementation.
Still, formal verification is not applicable to all the code, and to all the properties you want to check (in particular high-level properties, that cannot be easily expressed as contracts). This is why it is important to be able to combine testing and formal verification.