Automated test-data generation from formal models of software

Verification and Validation (V&V) of software for critical embedded control systems often consumes upto 70% of the development resources. Testing is one of the most frequently used V&V technique for verifying such systems. Many regulatory agencies that certify control systems for use require that the software be tested to certain specified levels of coverage. Currently, developing test cases to meet these requirements takes a major portion of the resources. Automating this task would result in significant time and cost savings. The objective of this paper is to automate the generation of such test cases. We propose an approach where we rely on a formal model of the required software behavior for test-case generation, as well as, an oracle to determine if the implementation produced the correct output during testing.