Sustaining Entire Code-Coverage on Code Optimization

The SECCO project is concerned with software testing, focusing in particular on the support of gray-box testing, i.e., testing methods where the source code of the program guides the test-data generation. Whenever an optimizing compiler is used, code coverage achieved at source-code level cannot guaranteed to be preserved at object-code level. Current practice is either to "live with this problem"` or to forbid code optimizations done by the compiler at all. The SECCO project aims to solve this problem of guaranteeing code coverage at object-code level by extending the compiler such that only those code optimizations are permitted that cannot disrupt the interested code coverage. Technically, this is done by proving for each code transformation whether it preserves the interested code-coverage criterion. To do this, the interested code-coverage criterion has to be specified formally and a coverage- preservation criterion has to be derived. In important industrial sectors such as the automotive industry, formal testing methods are starting to gain ground to ensure product quality and, most importantly, the safety of the passengers. The SECCO project provides the foundation for the formal generation of test-data at source-code level. Besides software testing, the SECCO project also improves the applicability of another important verification technique of real-time programs, the measurement- based timing analysis.

The SECCO project is concerned with software testing, focusing in particular on the support of gray-box testing, i.e., testing methods where the source code of the program guides the test-data generation. Whenever an optimizing compiler is used, code coverage achieved at source-code level cannot guaranteed to be preserved at object-code level. Current practice is either to "live with this problem" or to forbid code optimizations done by the compiler at all. The SECCO project aims to solve this problem of guaranteeing code coverage at object-code level by extending the compiler such that only those code optimizations are permitted that cannot disrupt the interested code coverage. Technically, this is done by proving for each code transformation whether it preserves the interested code-coverage criterion. To do this, the interested code-coverage criterion has to be specified formally and a coverage-preservation criterion has to be derived. In important industrial sectors such as the automotive industry, formal testing methods are starting to gain ground to ensure product quality and, most importantly, the safety of the passengers. The SECCO project provides the foundation for the formal generation of test-data at source-code level. Besides software testing, the SECCO project also improves the applicability of another important verification technique of real-time programs, the measurement-based timing analysis.