Industry Articles
Verifying embedded software functionality: Combining formal verification with testing-August 30, 2012 |
Abhik Roychoudhury
EETimes (8/29/2012 4:01 PM EDT)
Editor’s Note: In the final part in a four part series Abhik Roychoudhury, author of Embedded Systems and software validation, explains the usefulness of formal verification techniques to traditional software testing techniques.
As noted in Part 1 , Part 2, and Part 3 in this series, dynamic or trace-based checking methods are very useful for testing-oriented debugging. In other words, the software validation flow revolves around program testing—we test a program against selected test cases, and for the failed test cases (the ones for which the program output does not match the programmer’s “expectationsâ€), we analyze the traces for these test cases using dynamic checking methods.
However, program testing, by its very nature, is nonexhaustive. It is not feasible to test a program against all possible inputs. As a result, for safety-critical software it is crucial to employ checking methods that go beyond testing-oriented debugging. .
Currently, many functionalities in our daily lives are software controlled—functionalities that earlier used to be controlled by electrical/mechanical devices. Two specific application domains where software is increasingly being used to control critical functionalities are automotive and avionics. .