Verifying embedded software functionality: Combining formal verification with testing

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. .

Click here to read more ...