Integrating Proof and Testing in Verification Strategies for Safety Critical Systems

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.

This entry was posted in Open-DO News. Bookmark the permalink. Post a comment or leave a trackback: Trackback URL.

2 Comments

  1. Ram Cherukuri
    Posted April 26, 2013 at 20:15 | Permalink

    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

  2. Yannick Moy
    Posted May 15, 2013 at 14:26 | Permalink

    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.

Post a Comment

Your email is never published nor shared. Required fields are marked *

*
*
 
  • Categories

  • Open-DO Projects

  • Want to get involved?

  • Contact

    info @ open-do.org